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

% equality axioms:
all(x, eq_s(x,x)).
all(x, eq_c(x,x)).
all(x, eq_p(x,x)).

all(x, all(y, eq_s(x,y) iff eq_s(y,x))).
all(x, all(y, eq_c(x,y) iff eq_c(y,x))).
all(x, all(y, eq_p(x,y) iff eq_p(y,x))).

all(x, all(y, all(z, (eq_s(x,y) and eq_s(y,z)) imp eq_s(x,z)))).
all(x, all(y, all(z, (eq_c(x,y) and eq_c(y,z)) imp eq_c(x,z)))).
all(x, all(y, all(z, (eq_p(x,y) and eq_p(y,z)) imp eq_p(x,z)))).

% equality substitution axioms, PREDICATES:

all(x, all(y, all(z, (eq_c(x,y) and subset_c(x,z)) imp subset_c(y,z)))).
all(x, all(y, all(z, (eq_s(x,y) and subset_s(z,x)) imp subset_s(z,y)))).
all(x, all(y, all(z, (eq_s(x,y) and top_space(x,z)) imp
	top_space(y,z)))).
all(x, all(y, all(z, (eq_c(x,y) and top_space(z,x)) imp
	top_space(z,y)))).
all(x, all(y, (eq_c(x,y) and topology(x)) imp topology(y))).
all(x, all(y, all(z, (eq_s(x,y) and el_s(x,z)) imp el_s(y,z)))).
all(x, all(y, all(z, (eq_s(x,y) and el_p(z,x)) imp el_p(z,y)))).
all(x, all(y, all(z, (eq_c(x,y) and el_s(z,x)) imp el_s(z,y)))).
all(x, all(y, all(z, all(w, (eq_s(x,y) and open(x,z,w)) imp 
	open(y,z,w))))).
all(x, all(y, all(z, all(w, (eq_s(x,y) and open(z,x,w)) imp 
	open(z,y,w))))).
all(x, all(y, all(z, all(w, (eq_c(x,y) and open(w,z,x)) imp 
	open(w,z,y))))).
all(x, all(y, all(z, all(w, (eq_s(x,y) and closed(x,z,w)) imp 
	closed(y,z,w))))).
all(x, all(y, all(z, all(w, (eq_s(x,y) and closed(z,x,w)) imp 
	closed(z,y,w))))).
all(x, all(y, all(z, all(w, (eq_c(x,y) and closed(w,z,x)) imp 
	closed(w,z,y))))).
all(x, all(y, all(z, all(w, (eq_c(x,y) and finer(x,z,w)) imp 
	finer(y,z,w))))).
all(x, all(y, all(z, all(w, (eq_c(x,y) and finer(z,x,w)) imp 
	finer(z,y,w))))).
all(x, all(y, all(z, all(w, (eq_s(x,y) and finer(w,z,x)) imp 
	finer(w,z,y))))).
all(x, all(y, all(z, (eq_c(x,y) and basis(x,z)) imp basis(y,z)))).
all(x, all(y, all(z, (eq_s(x,y) and basis(z,x)) imp basis(z,y)))).
all(x, all(y, all(z, (eq_c(x,y) and subbasis(x,z)) imp subbasis(y,z)))).
all(x, all(y, all(z, (eq_s(x,y) and subbasis(z,x)) imp subbasis(z,y)))).
all(x, all(y, all(z, (eq_s(x,y) and hausdorff(x,z)) imp hausdorff(y,z)))).
all(x, all(y, all(z, (eq_c(x,y) and hausdorff(z,x)) imp hausdorff(z,y)))).
all(x, all(y, all(z, (eq_s(x,y) and tone(x,z)) imp tone(y,z)))).
all(x, all(y, all(z, (eq_c(x,y) and tone(z,x)) imp tone(z,y)))).
all(x, all(y, all(z, all(w, all(u, (eq_s(x,y) and 
	neighborhood(x,z,w,u)) imp neighborhood(y,z,w,u)))))).
all(x, all(y, all(z, all(w, all(u, (eq_p(x,y) and 
	neighborhood(z,x,w,u)) imp neighborhood(z,y,w,u)))))).
all(x, all(y, all(z, all(w, all(u, (eq_s(x,y) and 
	neighborhood(w,z,x,u)) imp neighborhood(w,z,y,u)))))).
all(x, all(y, all(z, all(w, all(u, (eq_c(x,y) and 
	neighborhood(u,z,w,x)) imp neighborhood(u,z,w,y)))))).
all(x, all(y, all(z, all(w, all(u, (eq_p(x,y) and 
	limit_pt(x,z,w,u)) imp limit_pt(y,z,w,u)))))).
all(x, all(y, all(z, all(w, all(u, (eq_s(x,y) and 
	limit_pt(z,x,w,u)) imp limit_pt(z,y,w,u)))))).
all(x, all(y, all(z, all(w, all(u, (eq_s(x,y) and 
	limit_pt(w,z,x,u)) imp limit_pt(w,z,y,u)))))).
all(x, all(y, all(z, all(w, all(u, (eq_c(x,y) and 
	limit_pt(u,z,w,x)) imp limit_pt(u,z,w,y)))))).

% equality substitution axioms, FUNCTIONS:

all(x, all(y, all(z, eq_s(x,y) imp
	eq_s(inter_s(x,z),inter_s(y,z))))).	
all(x, all(y, all(z, eq_c(x,y) imp
	eq_c(inter_c(x,z),inter_c(y,z))))).	
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_c(x,y) imp eq_s(sigma(x),sigma(y)))).
all(x, all(y, all(z, eq_s(x,y) imp
	eq_s(rel_comp(x,z),rel_comp(y,z))))).
all(x, all(y, all(z, eq_s(x,y) imp
	eq_s(rel_comp(z,x),rel_comp(z,y))))).
all(x, all(y, eq_c(x,y) imp eq_c(top_of_basis(x),top_of_basis(y)))).
all(x, all(y, eq_c(x,y) imp
	eq_c(top_of_subbasis(x),top_of_subbasis(y)))).
all(x, all(y, all(z, all(w, eq_s(x,y) imp
	eq_s(subspace_top(x,z,w),subspace_top(y,z,w)))))).
all(x, all(y, all(z, all(w, eq_c(x,y) imp
	eq_c(subspace_top(z,x,w),subspace_top(z,y,w)))))).
all(x, all(y, all(z, all(w, eq_s(x,y) imp
	eq_s(subspace_top(z,w,x),subspace_top(z,w,y)))))).
all(x, all(y, eq_s(x,y) imp eq_s(limit_pt_set(x),limit_pt_set(y)))).
all(x, all(y, all(z, all(w, eq_s(x,y) imp
	eq_s(boundary(x,z,w),boundary(y,z,w)))))).
all(x, all(y, all(z, all(w, eq_s(x,y) imp
	eq_s(boundary(z,x,w),boundary(z,y,w)))))).
all(x, all(y, all(z, all(w, eq_c(x,y) imp
	eq_s(boundary(w,z,x),boundary(w,z,y)))))).
all(x, all(y, all(z, all(w, eq_s(x,y) imp
	eq_s(interior(x,z,w),interior(y,z,w)))))).
all(x, all(y, all(z, all(w, eq_s(x,y) imp
	eq_s(interior(z,x,w),interior(z,y,w)))))).
all(x, all(y, all(z, all(w, eq_c(x,y) imp
	eq_s(interior(w,z,x),interior(w,z,y)))))).
all(x, all(y, all(z, all(w, eq_s(x,y) imp
	eq_s(closure(x,z,w),closure(y,z,w)))))).
all(x, all(y, all(z, all(w, eq_s(x,y) imp
	eq_s(closure(z,x,w),closure(z,y,w)))))).
all(x, all(y, all(z, all(w, eq_c(x,y) imp
	eq_s(closure(w,z,x),closure(w,z,y)))))).

% equality predicates:
all(x, all(y, eq_s(x,y) iff (subset_s(x,y) and subset_s(y,x)))).
all(x, all(y, eq_c(x,y) iff (subset_c(x,y) and subset_c(y,x)))).