% 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).