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

% description : 
% 
% AXIOMS FOR POINT-SET 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).

% closed set definition:

-closed(u,x,xt) | top_space(x,xt).
-closed(u,x,xt) | open(rel_comp(u,x),x,xt).
closed(u,x,xt) | -top_space(x,xt) | -open(rel_comp(u,x),x,xt).

% finer topology definition:

-finer(xt,xs,x) | top_space(x,xt).
-finer(xt,xs,x) | top_space(x,xs).
-finer(xt,xs,x) | subset_s(xs,xt).
finer(xt,xs,x) | -top_space(x,xt) | -top_space(x,xs) | -subset_s(xs,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_s(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_s(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).

% subbasis definition:

-subbasis(xs,x) | eq_s(sigma(xs),x).
subbasis(xs,x) | -eq_s(sigma(xs),x).

% topology generated by a subbasis definition:

-top_of_subbasis(xs,x,xt) | subbasis(xs,x).
-top_of_subbasis(xs,x,xt) | -subset(xs,xtemp) | el(f11(xs,x,xt,xtemp),xtemp) | 
	-subset(z,xtemp) | el(sigma(z),xt).
-top_of_subbasis(xs,x,xt) | -subset(xs,xtemp) | el(f12(xs,x,xt,xtemp),xtemp) | 
	-subset(z,xtemp) | el(sigma(z),xt).
-top_of_subbasis(xs,x,xt) | -subset(xs,xtemp) | 
	-el(intersect(f11(xs,x,xt,xtemp),f12(xs,x,xt,xtemp)),xtemp) | 
	-subset(z,xtemp) | el(sigma(z),xt).
top_of_subbasis(xs,x,xt) | -subbasis(xs,x) | subset(xs,f13(xs,x,xt)).
top_of_subbasis(xs,x,xt) | -subbasis(xs,x) | -el(uu12,f13(xs,x,xt)) | 
	-el(uu13,f13(xs,x,xt)) | el(intersect(uu12,uu13),f13(xs,x,xt)).
top_of_subbasis(xs,x,xt) | -subbasis(xs,x) | subset(f14(xs,x,xt),f13(xs,x,xt)).
top_of_subbasis(xs,x,xt) | -subbasis(xs,x) | -el(sigma(f14(xs,x,xt)),xt).

% subspace topology definition:

-el_s(u,subspace_top(x,xt,y)) | top_space(x,xt).
-el_s(u,subspace_top(x,xt,y)) | subset_s(y,x).
-el_s(u,subspace_top(x,xt,y)) | el_s(f15(x,xt,y,u),xt).
-el_s(u,subspace_top(x,xt,y)) | eq_s(u,inter_s(y,f15(x,xt,y,u))).
el_s(u,subspace_top(x,xt,y)) | -top_space(x,xt) | -subset_s(y,x) | 
	-el_s(uu15,xt) | -eq_s(u,inter_s(y,uu15)).

% interior definition:

-el_p(y,interior(ya,x,xt)) | top_space(x,xt).
-el_p(y,interior(ya,x,xt)) | subset_s(ya,x).
-el_p(y,interior(ya,x,xt)) | el_p(y,f16(ya,x,xt,y)).
-el_p(y,interior(ya,x,xt)) | subset_s(f16(ya,x,xt,y),ya).
-el_p(y,interior(ya,x,xt)) | open(f16(ya,x,xt,y),x,xt).
el_p(y,interior(ya,x,xt)) | -top_space(x,xt) | -subset_s(ya,x) | 
	-el_p(y,uu16) | -subset_s(uu16,ya) | -open(uu16,x,xt).

% closure definition:

-el_p(y,closure(ya,x,xt)) | top_space(x,xt).
-el_p(y,closure(ya,x,xt)) | subset_s(ya,x).
-el_p(y,closure(ya,x,xt)) | el_p(y,f17(ya,x,xt,y)).
-el_p(y,closure(ya,x,xt)) | subset_s(ya,f17(ya,x,xt,y)).
-el_p(y,closure(ya,x,xt)) | closed(f17(ya,x,xt,y),x,xt).
el_p(y,closure(ya,x,xt)) | -top_space(x,xt) | -subset_s(ya,x) | 
	-el_p(y,uu17) | -subset_s(ya,uu17) | -closed(uu17,x,xt).

% neighborhood def:

-neighborhood(u,xx,x,xt) | top_space(x,xt).
-neighborhood(u,xx,x,xt) | el_p(xx,x).
-neighborhood(u,xx,x,xt) | el_p(xx,u).
-neighborhood(u,xx,x,xt) | open(u,x,xt).
neighborhood(u,xx,x,xt) | -top_space(x,xt) | -el_p(xx,x) | -el_p(xx,u) | 
	-open(u,x,xt).

% limit point def:

-limit_pt(xx,ya,x,xt) | top_space(x,xt).
-limit_pt(xx,ya,x,xt) | el_p(xx,x).
-limit_pt(xx,ya,x,xt) | subset(ya,x).
-limit_pt(xx,ya,x,xt) | -neighborhood(u,xx,x,xt) | 
	el_p(f18(xx,ya,x,xt,u),intersect(u,ya)).
-limit_pt(xx,ya,x,xt) | -neighborhood(u,xx,x,xt) | -eq_p(f18(xx,ya,x,xt,u),x).
limit_pt(xx,ya,x,xt) | -top_space(x,xt) | -el_p(xx,x) | -subset(ya,x) | 
	neighborhood(f19(xx,ya,x,xt),xx,x,xt).
limit_pt(xx,ya,x,xt) | -top_space(x,xt) | -el_p(xx,x) | -subset(ya,x) | 
	-el_p(uu19,intersect(f19(xx,ya,x,xt),ya)) | eq_p(uu19,x).

% the set of limit points:

-eq_s(xa,limit_pt_set(ya)) | -el_p(xx,xa) | limit_pt(xx,ya,x,xt).
-eq_s(xa,limit_pt_set(ya)) | el_p(xx,xa) | -limit_pt(xx,ya,x,xt).
eq_s(xa,limit_pt_set(ya)) | el_p(f20(xa,ya,x,xt),xa) | 
	limit_pt(f20(xa,ya,x,xt),ya,x,xt).
eq_s(xa,limit_pt_set(ya)) | -el_p(f20(xa,ya,x,xt),xa) | 
	-limit_pt(f20(xa,ya,x,xt),ya,x,xt).

% hausdorff space definition:

-hausdorff(x,xt) | top_space(x,xt).
-hausdorff(x,xt) | -el_p(xx1,x) | -el_p(xx2,x) | eq_p(xx1,xx2) | 
	neighborhood(f21(x,xt,xx1,xx2),xx1,x,xt).
-hausdorff(x,xt) | -el_p(xx1,x) | -el_p(xx2,x) | eq_p(xx1,xx2) | 
	neighborhood(f22(x,xt,xx1,xx2),xx2,x,xt).
-hausdorff(x,xt) | -el_p(xx1,x) | -el_p(xx2,x) | eq_p(xx1,xx2) | 
	eq_s(inter_s(f21(x,xt,xx1,xx2),f22(x,xt,xx1,xx2)),0).
hausdorff(x,xt) | -top_space(x,xt) | el_p(f23(x,xt),x).
hausdorff(x,xt) | -top_space(x,xt) | el_p(f24(x,xt),x).
hausdorff(x,xt) | -top_space(x,xt) | -eq_p(f23(x,xt),f24(x,xt)).
hausdorff(x,xt) | -top_space(x,xt) | -neighborhood(uu23,f23(x,xt),x,xt) | 
	-neighborhood(uu24,f24(x,xt),x,xt) | -eq_s(inter_s(uu23,uu24),0).

% t-one axiom definition:

-tone(x,xt) | top_space(x,xt).
-tone(x,xt) | -el_p(xx1,x) | -el_p(xx2,x) | eq_p(xx1,xx2) | 
	neighborhood(f25(x,xt,xx1,xx2),xx1,x,xt).
-tone(x,xt) | -el_p(xx1,x) | -el_p(xx2,x) | eq_p(xx1,xx2) | 
	neighborhood(f26(x,xt,xx1,xx2),xx2,x,xt).
-tone(x,xt) | -el_p(xx1,x) | -el_p(xx2,x) | eq_p(xx1,xx2) | 
	-el_p(xx2,f25(x,xt,xx1,xx2)).
-tone(x,xt) | -el_p(xx1,x) | -el_p(xx2,x) | eq_p(xx1,xx2) | 
	-el_p(xx1,f26(x,xt,xx1,xx2)).
tone(x,xt) | -top_space(x,xt) | el_p(f27(x,xt),x).
tone(x,xt) | -top_space(x,xt) | el_p(f28(x,xt),x).
tone(x,xt) | -top_space(x,xt) | -eq_p(f27(x,xt),f28(x,xt)).
tone(x,xt) | -top_space(x,xt) | -neighborhood(uu27,f27(x,xt),x,xt) | 
	-neighborhood(uu28,f28(x,xt),x,xt) | el_p(f28(x,xt),uu27) | 
	el_p(f27(x,xt),uu28).


% boundary of a set def:

-el_p(xx,boundary(ya,x,xt)) | subset(ya,x).
-el_p(xx,boundary(ya,x,xt)) | el_p(xx,closure(ya,x,xt)).
-el_p(xx,boundary(ya,x,xt)) | el_p(xx,closure(rel_comp(ya,x),x,xt)).
el_p(xx,boundary(ya,x,xt)) | -subset(ya,x) | -el_p(xx,closure(ya,x,xt)) | 
	-el_p(xx,closure(rel_comp(ya,x),x,xt)).