let Y be non empty TopStruct ; :: thesis: for A being non empty Subset of Y holds Sspace A is SubSpace of MaxADSspace A
let A be non empty Subset of Y; :: thesis: Sspace A is SubSpace of MaxADSspace A
( the carrier of (MaxADSspace A) = MaxADSet A & A c= MaxADSet A & the carrier of (Sspace A) = A ) by Def19, Lm3, Th34;
hence Sspace A is SubSpace of MaxADSspace A by Lm2; :: thesis: verum