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