% problem-set/topology/point.set/defs.first_order
% created : 08/04/88
% revised : 08/18/89

% top_space definition:
all(x, all(xt, top_space(x,xt) iff (

	el_s(0,xt) and
	el_s(x,xt) and

	all(y, all(w, el_s(y,xt) and el_s(w,xt) imp el_s(inter_s(y,w), xt)))
		and 

	all(z, subset_s(z,xt) imp el_s(sigma(z), xt))
))). 

% topology definition:
all(xt, topology(xt) iff exists(x, top_space(x,xt))).

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

% open set definition:
all(u, all(x, all(xt, open(u,x,xt) iff top_space(x,xt) and el_s(u,xt)))).

% closed set definition:
all(u, all(x, all(xt, closed(u,x,xt) iff

	top_space(x,xt) and open(rel_comp(u, x), x, xt)))).

% finer topology definition:
all(xt, all(xs, all(x, finer(xt,xs,x) iff 

	top_space(x, xt) and top_space(x, xs) and subset_s(xs, xt)))).

% basis for a topology definition:
all(xb, all(x, basis(xb,x) iff

	(eq_s(sigma(xb),x) and 

	all(xx, el_p(xx,x) imp ( all(xb1, all(xb2, 
		( el_s(xb1,xb) and el_s(xb2,xb) 
		and el_p(xx,inter_s(xb1,xb2)) )
		imp exists(xb3, (el_s(xb3,xb) and el_p(xx,xb3) and
			subset_s(xb3,inter_s(xb1,xb2))))
	)))))
)). 

% topology generated by a basis definition:
all(xb, all(u, el_s(u,top_of_basis(xb)) iff
	all(x, el_p(x,u) imp exists(z, el_s(z,xb) and el_p(x,z) and
		subset_s(z,u)))
)).

% subbasis definition:
all(xs, all(x, subbasis(xs,x) iff eq_s(sigma(xs),x) )).

% topology generated by a subbasis definition:
all(xs, all(x, all(xt, top_of_subbasis(xs,x,xt) iff

	subbasis(xs,x) and
	all(xtemp, ( subset(xs,xtemp) and all(yt1, all(yt2, 
			(el(yt1,xtemp) and el(yt2,xtemp)) imp
			el(intersect(yt1,yt2),xtemp) )) )
		imp all(z, subset(z,xtemp) imp el(sigma(z), xt)))
))).

% subspace topology definition:
all(x, all(xt, all(y, all(u, el_s(u,subspace_top(x,xt,y)) iff
	(top_space(x,xt) and subset_s(y,x) and 
	exists(vt, (el_s(vt,xt) and eq_s(u,inter_s(y,vt)))
	))
)))).

% interior definition:

all(ya, all(x, all(xt, all(y, el_p(y,interior(ya,x,xt)) iff
	( top_space(x,xt) and subset_s(ya,x) and 
	exists(v, (el_p(y, v) and subset_s(v,ya) and open(v,x,xt))
	))
)))).

% closure definition:

all(ya, all(x, all(xt, all(y, el_p(y,closure(ya,x,xt)) iff
	( top_space(x,xt) and subset_s(ya,x) and 
	exists(v, (el_p(y, v) and subset_s(ya,v) and closed(v,x,xt))
	))
)))).

% neighborhood def:

all(u, all(x, all(xx, all(xt, neighborhood(u,xx,x,xt) iff
	( top_space(x,xt) and el_p(xx,x) and el_p(xx,u) 
	and open(u,x,xt))
)))).

% limit point def:

all(xx, all(ya, all(x, all(xt, limit_pt(xx,ya,x,xt) iff
	( top_space(x,xt) and el_p(xx,x) and subset(ya,x) and
	all(u, neighborhood(u,xx,x,xt) imp exists(y, 
		el_p(y,intersect(u,ya)) and ~eq_p(y,x))
	))
)))).

% the set of limit points:

all(xa, all(ya, all(x, all(xt, eq_s(xa,limit_pt_set(ya)) iff
	all(xx, el_p(xx,xa) iff limit_pt(xx,ya,x,xt))
)))).

% hausdorff space definition:

all(x, all(xt, hausdorff(x,xt) iff ( top_space(x,xt) and
	all(xx1, all(xx2, (el_p(xx1,x) and el_p(xx2,x) and ~eq_p(xx1,xx2)) 
		imp exists(u1, exists(u2, ( neighborhood(u1,xx1,x,xt)
		and neighborhood(u2,xx2,x,xt) and 
		eq_s(inter_s(u1,u2),0) )
	))))
))).


% t-one axiom definition:

all(x, all(xt, tone(x,xt) iff ( top_space(x,xt) and 
	all(xx1, all(xx2, (el_p(xx1,x) and el_p(xx2,x) and ~eq_p(xx1,xx2)) 
		imp exists(u1, exists(u2, ( neighborhood(u1,xx1,x,xt)
		and neighborhood(u2,xx2,x,xt) and 
		~el_p(xx2,u1) and ~el_p(xx1,u2))
	))))
))).


% boundary of a set def:

all(x, all(xt, all(ya, all(xx, el_p(xx,boundary(ya,x,xt)) iff
	( subset(ya,x) and el_p(xx,closure(ya,x,xt)) and
	el_p(xx,closure(rel_comp(ya,x),x,xt)) )
)))).