% problem-set/topology/point.set/lemma17.clauses % created : 08/08/88 % revised : 08/17/89 % description : % % lemma 17: Let ya be a subset of x, (x,xt) a topological space. Then % (a) xx is in ya closure iff for all open subsets u of x for % which xx is in u, u intersect ya is not empty and % (b) xx is in ya closure and xb is a basis for x iff for all % yb in xb such that xx is in yb, yb intersect ya is not empty. % representation : % % See axioms.decl for a full explanation. % denial: el_p(P,closure(A,X,T)) | -subset_s(u,X) | -open(u,X,T) | -el_p(P,u) | -eq_s(intersect(u,A),0) | -el_s(yb,B) | -el_p(P,yb) | -eq_s(intersect(yb,A),0). el_p(P,closure(A,X,T)) | -subset_s(u,X) | -open(u,X,T) | -el_p(P,u) | -eq_s(intersect(u,A),0) | basis(B,X) | -el_s(yb,B) | -el_p(P,yb) | -eq_s(intersect(yb,A),0). -el_p(P,closure(A,X,T)) | subset_s(V,X) | basis(B,X) | -el_s(yb,B) | -el_p(P,yb) | -eq_s(intersect(yb,A),0). -el_p(P,closure(A,X,T)) | subset_s(V,X) | -basis(B,X) | el_s(C,B). -el_p(P,closure(A,X,T)) | subset_s(V,X) | -basis(B,X) | el_p(P,C). -el_p(P,closure(A,X,T)) | subset_s(V,X) | -basis(B,X) | eq_s(intersect(C,A),0). -el_p(P,closure(A,X,T)) | open(V,X,T) | basis(B,X) | -el_s(yb,B) | -el_p(P,yb) | -eq_s(intersect(yb,A),0). -el_p(P,closure(A,X,T)) | open(V,X,T) | -basis(B,X) | el_s(C,B). -el_p(P,closure(A,X,T)) | open(V,X,T) | -basis(B,X) | el_p(P,C). -el_p(P,closure(A,X,T)) | open(V,X,T) | -basis(B,X) | eq_s(intersect(C,A),0). -el_p(P,closure(A,X,T)) | el_p(P,V) | basis(B,X) | -el_s(yb,B) | -el_p(P,yb) | -eq_s(intersect(yb,A),0). -el_p(P,closure(A,X,T)) | el_p(P,V) | -basis(B,X) | el_s(C,B). -el_p(P,closure(A,X,T)) | el_p(P,V) | -basis(B,X) | el_p(P,C). -el_p(P,closure(A,X,T)) | el_p(P,V) | -basis(B,X) | eq_s(intersect(C,A),0). -el_p(P,closure(A,X,T)) | eq_s(intersect(V,A),0) | basis(B,X) | -el_s(yb,B) | -el_p(P,yb) | -eq_s(intersect(yb,A),0). -el_p(P,closure(A,X,T)) | eq_s(intersect(V,A),0) | -basis(B,X) | el_s(C,B). -el_p(P,closure(A,X,T)) | eq_s(intersect(V,A),0) | -basis(B,X) | el_p(P,C). -el_p(P,closure(A,X,T)) | eq_s(intersect(V,A),0) | -basis(B,X) | eq_s(intersect(C,A),0).