let Y be non empty TopStruct ; :: thesis: for Y0 being SubSpace of Y
for A being non empty Subset of Y st A is Subset of Y0 holds
Sspace A is SubSpace of Y0
let Y0 be SubSpace of Y; :: thesis: for A being non empty Subset of Y st A is Subset of Y0 holds
Sspace A is SubSpace of Y0
let A be non empty Subset of Y; :: thesis: ( A is Subset of Y0 implies Sspace A is SubSpace of Y0 )
assume A is Subset of Y0 ; :: thesis: Sspace A is SubSpace of Y0
then A c= the carrier of Y0 ;
then the carrier of (Sspace A) c= the carrier of Y0 by Lm3;
hence Sspace A is SubSpace of Y0 by Lm2; :: thesis: verum