% problem-set/topology/point.set/lemma5.clauses % created : 08/08/88 % revised : 08/17/89 % description : % % lemma: If y is a subspace of x, u is an open subset of y, y is. % open in x, then u is open in x. % representation : % % See axioms.decl for a full explanation. % denial: exists y a subspace of x with u an open subset of y. % such that y is open in x but u is not open in x. subset(Y,X). open(U,Y,subspace_top(X,T,Y)). open(Y,X,T). -open(U,X,T).