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

% set theory axioms & lemmas.

all(x, subset_s(0,x)).
all(x, ~el_s(x,0)).
all(x, ~el_p(x,0)).
all(x, subset_s(x,x)).
all(x, subset_c(x,x)).
all(x, all(y, all(z, (subset_s(x,y) and subset_s(y,z)) imp subset_s(x,z)))).
all(x, all(y, all(z, (subset_c(x,y) and subset_c(y,z)) imp subset_c(x,z)))).

all(z, all(x, el_p(z,sigma(x)) iff exists(y, el_s(y,x) and el_p(z,y)))).
all(z, all(x, el_p(z,tau(x)) iff all(y, el_s(y,x) imp el_p(z,y)))).
all(x, all(y, el_s(x,y) imp subset_s(x,sigma(y)))).
all(x, all(y, all(z, (subset_s(x,y) and el_s(y,z)) imp subset_s(x,sigma(z))))).

all(u, all(x, eq_s(inter_s(u,rel_comp(u,x)),0))).
all(u, all(x, eq_s(join_s(u,rel_comp(u,x)),x))).
all(u, all(x, eq_s(inter_s(rel_comp(u,x),u),0))).
all(u, all(x, eq_s(join_s(rel_comp(u,x),u),x))).
all(x, all(u, all(y, el_p(y,x) imp (el_p(y,u) iff ~el_p(y,rel_comp(u,x)))))).

all(x, all(y, subset_s(x,y) iff all(u, el_p(u,x) imp el_p(u,y)))).
all(x, all(y, subset_c(x,y) iff all(u, el_s(u,x) imp el_s(u,y)))).

all(x, all(y, all(z, el_s(z, inter_c(x,y)) iff (el_s(z,x) and el_s(z,y))))).
all(x, all(y, all(z, el_p(z, inter_s(x,y)) iff (el_p(z,x) and el_p(z,y))))).
all(x, all(y, all(z, el_s(z, join_c(x,y)) iff (el_s(z,x) or el_s(z,y))))).
all(x, all(y, all(z, el_p(z, join_s(x,y)) iff (el_p(z,x) or el_p(z,y))))).
all(x, all(y, all(u, all(v, (subset_s(x,y) and subset_s(u,v)) imp 
	(subset_s(inter_c(x,u),inter_c(y,v))))))).
all(x, all(y, all(u, all(v, (subset_c(x,y) and subset_c(u,v)) imp 
	(subset_c(inter_c(x,u),inter_c(y,v))))))).

all(x1, all(x2, all(y1, all(y2, (subset_s(x1,y1) and subset_s(x2,y2)) imp
	subset_s(inter_s(x1,x2),inter_s(y1,y2)))))).