% problem-set/topology/point.set/lemma1c.clauses % created : 08/08/88 % revised : 08/17/89 % description : % % lemma 1c: If xb is a basis for x, then for any u,v in the topology % generated by xb, u inter_s v is also in the topology. % representation : % % See axioms.decl for a full explanation. -basis(xb,x) | eq_s(sigma(xb),x). -basis(xb,x) | -el_p(xx,x) | -el_s(xb1,xb) | -el_s(xb2,xb) | -el_p(xx,inter_s(xb1,xb2)) | el_s(f3(xb,x,xx,xb1,xb2),xb). -basis(xb,x) | -el_p(xx,x) | -el_s(xb1,xb) | -el_s(xb2,xb) | -el_p(xx,inter_s(xb1,xb2)) | el_p(xx,f3(xb,x,xx,xb1,xb2)). -basis(xb,x) | -el_p(xx,x) | -el_s(xb1,xb) | -el_s(xb2,xb) | -el_p(xx,inter_s(xb1,xb2)) | subset_s(f3(xb,x,xx,xb1,xb2),inter_s(xb1,xb2)). % topology generated by a basis definition: -el_s(u,top_of_basis(xb)) | -el_p(x,u) | el_s(f7(xb,u,x),xb). -el_s(u,top_of_basis(xb)) | -el_p(x,u) | el_p(x,f7(xb,u,x)). -el_s(u,top_of_basis(xb)) | -el_p(x,u) | subset_s(f7(xb,u,x),u). el_s(u,top_of_basis(xb)) | el_p(f8(xb,u),u). el_s(u,top_of_basis(xb)) | -el_s(uu10,xb) | -el_p(f8(xb,u),uu10) | -subset_s(uu10,u). % set theory axioms & lemmas. -subset_s(x,y) | -subset_s(y,z) | subset_s(x,z). eq_s(inter_s(x,y),inter_s(y,x)). -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). -subset_s(x,y) | -subset_s(u,v) | subset_s(inter_s(x,u),inter_s(y,v)). -el_s(u,x) | -el_p(z,u) | el_p(z,sigma(x)). -eq_s(x,y) | -el_p(z,x) | el_p(z,y). % denial: basis(B,X). el_s(U,top_of_basis(B)). el_s(V,top_of_basis(B)). -el_s(inter_s(U,V),top_of_basis(B)). eq_s(inter_s(x,inter_s(y,z)), inter_s(y,inter_s(x,z))). eq_s(inter_s(x,y),inter_s(y,x)). eq_s(inter_s(0,x),0). eq_s(inter_s(x,x),x). eq_s(inter_s(x,inter_s(x,y)),inter_s(x,y)). eq_s(inter_s(X,x), x).