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

% description : 
% 
% lemma 13: If y is a subspace of x, then ya a subset of y is closed 
%	iff ya=xc intersect y, where xc is closed in x.

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

% denial: 

closed(A,Y,subspace_top(X,T,Y)) | closed(C,X,T).
closed(A,Y,subspace_top(X,T,Y)) | eq_s(A,intersect(C,Y)).
-closed(A,Y,subspace_top(X,T,Y)) | -closed(uu1,X,T) | 
	-eq_s(A,intersect(uu1,Y)).

