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

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