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

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