let Y be non empty TopStruct ; :: thesis: for A, B being non empty Subset of Y st A is Subset of (MaxADSspace B) holds
MaxADSspace A is SubSpace of MaxADSspace B
let A, B be non empty Subset of Y; :: thesis: ( A is Subset of (MaxADSspace B) implies MaxADSspace A is SubSpace of MaxADSspace B )
A1: ( the carrier of (MaxADSspace A) = MaxADSet A & the carrier of (MaxADSspace B) = MaxADSet B ) by Def19;
assume A is Subset of (MaxADSspace B) ; :: thesis: MaxADSspace A is SubSpace of MaxADSspace B
hence MaxADSspace A is SubSpace of MaxADSspace B by A1, Lm2, Th36; :: thesis: verum