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

% description : 
% 
% set theory axioms & lemmas

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

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

subset_s(0,x).
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_p(z,tau(x)) | -el_s(y,x) | el_p(z,y).
el_p(z,tau(x)) | el_s(g2(z,x),x).
el_p(z,tau(x)) | -el_p(z,g2(z,x)).

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

eq_s(inter_s(u,rel_comp(u,x)),0).
eq_s(join_s(u,rel_comp(u,x)),x).
eq_s(inter_s(rel_comp(u,x),u),0).
eq_s(join_s(rel_comp(u,x),u),x).

-el_p(y,x) | -el_p(y,u) | -el_p(y,rel_comp(u,x)).
-el_p(y,x) | el_p(y,u) | el_p(y,rel_comp(u,x)).

-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_s(z,inter_c(x,y)) | el_s(z,x).
-el_s(z,inter_c(x,y)) | el_s(z,y).
el_s(z,inter_c(x,y)) | -el_s(z,x) | -el_s(z,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(x,y) | -subset_s(u,v) | subset_s(inter_c(x,u),inter_c(y,v)).
-subset_c(x,y) | -subset_c(u,v) | subset_c(inter_c(x,u),inter_c(y,v)).
-subset_s(x1,y1) | -subset_s(x2,y2) | subset_s(inter_s(x1,x2),inter_s(y1,y2)).