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

all(xt, eq_s(g4(xt),sigma(xt))).
all(x, all(y, eq_s(inter_s(x,y),inter_s(y,x)))).
all(x, all(y, eq_c(inter_c(x,y),inter_c(y,x)))).
all(x, all(y, eq_s(join_s(x,y),join_s(y,x)))).
all(x, all(y, eq_c(join_c(x,y),join_c(y,x)))).
all(x, all(u, eq_s(inter_s(u,rel_comp(u,x)),0))).
all(x, all(u, eq_s(join_s(u,rel_comp(u,x)),x))).
all(x, all(u, eq_s(inter_s(rel_comp(u,x),u),0))).
all(x, all(u, eq_s(join_s(rel_comp(u,x),u),x))).
all(x, all(y, all(z, 
	eq_s(inter_s(inter_s(x,y),z), inter_s(x,inter_s(y,z)))))).
all(x, all(y, all(z, 
	eq_c(inter_c(inter_c(x,y),z), inter_c(x,inter_c(y,z)))))).
all(x, all(y, all(z,
	eq_s(join_s(join_s(x,y),z), join_s(x,join_s(y,z)))))).
all(x, all(y, all(z,
	eq_c(join_c(join_c(x,y),z), join_c(x,join_c(y,z)))))).
all(x, eq_s(inter_s(x,x),x)).
all(x, eq_s(inter_s(x,0),0)).
all(x, eq_s(inter_s(0,x),0)).
all(x, eq_s(join_s(x,x),x)).
all(x, eq_s(join_s(x,0),x)).
all(x, eq_s(join_s(0,x),x)).
all(x, all(y, eq_s(inter_s(x,inter_s(x,y)),inter_s(x,y)))).
all(x, all(y, eq_c(inter_c(x,inter_c(x,y)),inter_c(x,y)))).
all(x, all(y, eq_s(inter_s(x,inter_s(y,x)),inter_s(x,y)))).
all(x, all(y, eq_c(inter_c(x,inter_c(y,x)),inter_c(x,y)))).
all(x, all(y, eq_s(join_s(x,join_s(x,y)),join_s(x,y)))).
all(x, all(y, eq_c(join_c(x,join_c(x,y)),join_c(x,y)))).
all(x, all(y, eq_s(join_s(x,join_s(y,x)),join_s(x,y)))).
all(x, all(y, eq_c(join_c(x,join_c(y,x)),join_c(x,y)))).