let Y be non empty TopStruct ; :: thesis: for A being non empty Subset of Y holds A is Subset of (Sspace A)
let A be non empty Subset of Y; :: thesis: A is Subset of (Sspace A)
the carrier of (Sspace A) c= the carrier of (Sspace A) ;
hence A is Subset of (Sspace A) by Lm3; :: thesis: verum