% problem-set/topology/point.set/lemma9.clauses % created : 08/08/88 % revised : 08/17/89 % description : % % lemma 9: let x be a set, xb1 a basis for the topology xt1 on x, xb2 a basis % for the topology xt2 on x. then xt2 is finer than xt1 iff for all % xx in x, every basis element around xx found in xb1 contains a basis % element around xx found in xb2. % representation : % % See axioms.decl for a full explanation. % denial: basis(B1,X). basis(B2,X). eq_c(top_of_basis(B1),top_of_basis(B1)). eq_c(top_of_basis(B2),top_of_basis(B2)). finer(top_of_basis(B2),top_of_basis(B1),X) | -el_p(xx,X) | -el_p(xx,u) | -el_s(u,B1) | el_p(xx,h1(xx,u)). finer(top_of_basis(B2),top_of_basis(B1),X) | -el_p(xx,X) | -el_p(xx,u) | -el_s(u,B1) | el_s(h1(xx,u),B2). finer(top_of_basis(B2),top_of_basis(B1),X) | -el_p(xx,X) | -el_p(xx,u) | -el_s(u,B1) | subset_s(h1(xx,u),u). -finer(top_of_basis(B2),top_of_basis(B1),X) | el_p(P,X). -finer(top_of_basis(B2),top_of_basis(B1),X) | el_p(P,C). -finer(top_of_basis(B2),top_of_basis(B1),X) | el_s(C,B1). -finer(top_of_basis(B2),top_of_basis(B1),X) | -el_p(P,uu3) | -el_s(uu3,B2) | -subset_s(uu3,C).