let Y be non empty TopStruct ; :: thesis: for Y0 being SubSpace of Y
for A being non empty Subset of st A is Subset of holds
Sspace A is SubSpace of Y0
let Y0 be SubSpace of Y; :: thesis: for A being non empty Subset of st A is Subset of holds
Sspace A is SubSpace of Y0
let A be non empty Subset of ; :: thesis: ( A is Subset of implies Sspace A is SubSpace of Y0 )
assume A is Subset of ; :: 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