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
A1: the carrier of (Sspace A) = A by Lm3;
the carrier of (MaxADSspace A) = MaxADSet A by Def18;
hence Sspace A is SubSpace of MaxADSspace A by A1, Lm2, Th32; :: thesis: verum