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

% description : 
% 
% equivalent definition of top_of_basis: 

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

% denial: 

el(f2,top_of_basis(f1)) | subset(f3,f1).
el(f2,top_of_basis(f1)) | equal(f2,sigma(f3)).
-el(f2,top_of_basis(f1)) | -subset(uu1,f1) | -equal(f2,sigma(uu1)).