% problem-set/topology/point.set/lemma1d.clauses
% created : 08/08/88
% revised : 08/17/89

% description : 
% 
% lemma 1d: If xb is a basis for x, then for any subset u of the topology
%	generated by xb, sigma(u) is also in the topology.

% representation : 
%
% See axioms.decl for a full explanation.

% top_space definition:

-top_space(x,xt) | el_s(0,xt).
-top_space(x,xt) | el_s(x,xt).
-top_space(x,xt) | -el_s(y,xt) | -el_s(w,xt) | el_s(inter_s(y,w),xt).
-top_space(x,xt) | -subset_s(z,xt) | el_s(sigma(z),xt).
top_space(x,xt) | -el_s(0,xt) | -el_s(x,xt) | el_s(f1(x,xt),xt) | 
	subset_s(f3(x,xt),xt).
top_space(x,xt) | -el_s(0,xt) | -el_s(x,xt) | el_s(f1(x,xt),xt) | 
	-el_s(sigma(f3(x,xt)),xt).
top_space(x,xt) | -el_s(0,xt) | -el_s(x,xt) | el_s(f2(x,xt),xt) | 
	subset_s(f3(x,xt),xt).
top_space(x,xt) | -el_s(0,xt) | -el_s(x,xt) | el_s(f2(x,xt),xt) | 
	-el_s(sigma(f3(x,xt)),xt).
top_space(x,xt) | -el_s(0,xt) | -el_s(x,xt) | 
	-el_s(inter_s(f1(x,xt),f2(x,xt)),xt) | subset_s(f3(x,xt),xt).
top_space(x,xt) | -el_s(0,xt) | -el_s(x,xt) | 
	-el_s(inter_s(f1(x,xt),f2(x,xt)),xt) | -el_s(sigma(f3(x,xt)),xt).

% topology definition:

-topology(xt) | top_space(f4(xt),xt).
topology(xt) | -top_space(uu4,xt).

eq_s(f4(xt),sigma(xt)).

% open set definition:

-open(u,x,xt) | top_space(x,xt).
-open(u,x,xt) | el_s(u,xt).
open(u,x,xt) | -top_space(x,xt) | -el_s(u,xt).

% basis for a topology definition:

-basis(xb,x) | eq_s(sigma(xb),x).
-basis(xb,x) | -el_p(xx,x) | -el_s(xb1,xb) | -el_s(xb2,xb) | 
	-el_p(xx,inter_s(xb1,xb2)) | el_p(f5(xb,x,xx,xb1,xb2),xb).
-basis(xb,x) | -el_p(xx,x) | -el_s(xb1,xb) | -el_s(xb2,xb) | 
	-el_p(xx,inter_s(xb1,xb2)) | el_p(xx,f5(xb,x,xx,xb1,xb2)).
-basis(xb,x) | -el_p(xx,x) | -el_s(xb1,xb) | -el_s(xb2,xb) | 
	-el_p(xx,inter_s(xb1,xb2)) | 
	subset_s(f5(xb,x,xx,xb1,xb2),inter_s(xb1,xb2)).
basis(xb,x) | -eq_s(sigma(xb),x) | el_p(f6(xb,x),x).
basis(xb,x) | -eq_s(sigma(xb),x) | el_s(f7(xb,x),xb).
basis(xb,x) | -eq_s(sigma(xb),x) | el_s(f8(xb,x),xb).
basis(xb,x) | -eq_s(sigma(xb),x) | el_p(f6(xb,x),inter_s(f7(xb,x),f8(xb,x))).
basis(xb,x) | -eq_s(sigma(xb),x) | -el_p(uu8,xb) | -el_p(f6(xb,x),uu8) | 
	-subset_s(uu8,inter_s(f7(xb,x),f8(xb,x))).

% topology generated by a basis definition:

-el_s(u,top_of_basis(xb)) | -el_p(x,u) | el_s(f9(xb,u,x),xb).
-el_s(u,top_of_basis(xb)) | -el_p(x,u) | el_p(x,f9(xb,u,x)).
-el_s(u,top_of_basis(xb)) | -el_p(x,u) | subset_s(f9(xb,u,x),u).
el_s(u,top_of_basis(xb)) | el_p(f10(xb,u),u).
el_s(u,top_of_basis(xb)) | -el_s(uu10,xb) | -el_p(f10(xb,u),uu10) | 
	-subset_s(uu10,u).

% set theory axioms & lemmas.

subset_s(0,x).
-el_s(x,0).
-el_p(x,0).
subset_s(x,x).
subset_c(x,x).

-subset_s(x,y) | -subset_s(y,z) | subset_s(x,z).
-subset_c(x,y) | -subset_c(y,z) | subset_c(x,z).

-el_p(z,sigma(x)) | el_s(g1(z,x),x).
-el_p(z,sigma(x)) | el_p(z,g1(z,x)).
el_p(z,sigma(x)) | -el_s(uu1,x) | -el_p(z,uu1).

-el_s(x,y) | subset_s(x,sigma(y)).
-subset_s(x,y) | -el_s(y,z) | subset_s(x,sigma(z)).

-subset_s(x,y) | -el_p(u,x) | el_p(u,y).
subset_s(x,y) | el_p(g3(x,y),x).
subset_s(x,y) | -el_p(g3(x,y),y).

-subset_c(x,y) | -el_s(u,x) | el_s(u,y).
subset_c(x,y) | el_s(g4(x,y),x).
subset_c(x,y) | -el_s(g4(x,y),y).

-el_p(z,inter_s(x,y)) | el_p(z,x).
-el_p(z,inter_s(x,y)) | el_p(z,y).
el_p(z,inter_s(x,y)) | -el_p(z,x) | -el_p(z,y).

-el_s(z,join_c(x,y)) | el_s(z,x) | el_s(z,y).
el_s(z,join_c(x,y)) | -el_s(z,x).
el_s(z,join_c(x,y)) | -el_s(z,y).

-el_p(z,join_s(x,y)) | el_p(z,x) | el_p(z,y).
el_p(z,join_s(x,y)) | -el_p(z,x).
el_p(z,join_s(x,y)) | -el_p(z,y).

-subset_s(x1,y1) | -subset_s(x2,y2) | subset_s(inter_s(x1,x2),inter_s(y1,y2)).

% equality axioms:

eq_s(x,x).
eq_c(x,x).
eq_p(x,x).

-eq_s(x,y) | eq_s(y,x).
eq_s(x,y) | -eq_s(y,x).
-eq_s(x,y) | -eq_s(y,z) | eq_s(x,z).
-eq_c(x,y) | eq_c(y,x).
eq_c(x,y) | -eq_c(y,x).
-eq_c(x,y) | -eq_c(y,z) | eq_c(x,z).
-eq_p(x,y) | eq_p(y,x).
eq_p(x,y) | -eq_p(y,x).
-eq_p(x,y) | -eq_p(y,z) | eq_p(x,z).

% equality substitution axioms:

-eq_c(x,y) | -subset_c(x,z) | subset_c(y,z).
-eq_s(x,y) | -subset_s(z,x) | subset_s(z,y).

-eq_s(x,y) | -top_space(x,z) | top_space(y,z).
-eq_c(x,y) | -top_space(z,x) | top_space(z,y).

-eq_c(x,y) | -topology(x) | topology(y).

-eq_s(x,y) | -el_s(x,z) | el_s(y,z).
-eq_s(x,y) | -el_p(z,x) | el_p(z,y).
-eq_c(x,y) | -el_s(z,x) | el_s(z,y).

-eq_s(x,y) | -open(x,z,w) | open(y,z,w).
-eq_s(x,y) | -open(z,x,w) | open(z,y,w).
-eq_c(x,y) | -open(w,z,x) | open(w,z,y).

-eq_c(x,y) | -basis(x,z) | basis(y,z).
-eq_s(x,y) | -basis(z,x) | basis(z,y).

-eq_s(x,y) | eq_s(inter_s(x,z),inter_s(y,z)).
eq_s(inter_s(x,y),inter_s(y,x)).

-eq_c(x,y) | eq_s(sigma(x),sigma(y)).
-eq_c(x,y) | eq_c(top_of_basis(x),top_of_basis(y)).

% equality predicates:

-eq_s(x,y) | subset_s(x,y).
-eq_s(x,y) | subset_s(y,x).
eq_s(x,y) | -subset_s(x,y) | -subset_s(y,x).

-eq_c(x,y) | subset_c(x,y).
-eq_c(x,y) | subset_c(y,x).
eq_c(x,y) | -subset_c(x,y) | -subset_c(y,x).

% denial:

subset_c(U,top_of_basis(B)).
-el_s(sigma(U),top_of_basis(B)).

eq_s(f4(xt),sigma(xt)).
eq_s(inter_s(x,y),inter_s(y,x)).
eq_c(inter_c(x,y),inter_c(y,x)).
eq_s(join_s(x,y),join_s(y,x)).
eq_c(join_c(x,y),join_c(y,x)).
eq_s(inter_s(inter_s(x,y),z), inter_s(x,inter_s(y,z))).
eq_c(inter_c(inter_c(x,y),z), inter_c(x,inter_c(y,z))).
eq_s(join_s(join_s(x,y),z), join_s(x,join_s(y,z))).
eq_c(join_c(join_c(x,y),z), join_c(x,join_c(y,z))).
eq_s(inter_s(x,x),x).
eq_s(inter_s(x,0),0).
eq_s(inter_s(0,x),0).
eq_s(join_s(x,x),x).
eq_s(join_s(x,0),x).
eq_s(join_s(0,x),x).
eq_s(inter_s(x,inter_s(x,y)),inter_s(x,y)).
eq_c(inter_c(x,inter_c(x,y)),inter_c(x,y)).
eq_s(inter_s(x,inter_s(y,x)),inter_s(x,y)).
eq_c(inter_c(x,inter_c(y,x)),inter_c(x,y)).
eq_s(join_s(x,join_s(x,y)),join_s(x,y)).
eq_c(join_c(x,join_c(x,y)),join_c(x,y)).
eq_s(join_s(x,join_s(y,x)),join_s(x,y)).
eq_c(join_c(x,join_c(y,x)),join_c(x,y)).