let Y be non empty TopStruct ; :: thesis: for A, B being non empty Subset of Y st A c= B holds

MaxADSspace A is SubSpace of MaxADSspace B

let A, B be non empty Subset of Y; :: thesis: ( A c= B implies MaxADSspace A is SubSpace of MaxADSspace B )

assume A1: A c= B ; :: thesis: MaxADSspace A is SubSpace of MaxADSspace B

A2: the carrier of (MaxADSspace B) = MaxADSet B by Def18;

the carrier of (MaxADSspace A) = MaxADSet A by Def18;

hence MaxADSspace A is SubSpace of MaxADSspace B by A2, A1, Lm2, Th31; :: thesis: verum

MaxADSspace A is SubSpace of MaxADSspace B

let A, B be non empty Subset of Y; :: thesis: ( A c= B implies MaxADSspace A is SubSpace of MaxADSspace B )

assume A1: A c= B ; :: thesis: MaxADSspace A is SubSpace of MaxADSspace B

A2: the carrier of (MaxADSspace B) = MaxADSet B by Def18;

the carrier of (MaxADSspace A) = MaxADSet A by Def18;

hence MaxADSspace A is SubSpace of MaxADSspace B by A2, A1, Lm2, Th31; :: thesis: verum