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 by Def18;
hence A is Subset of (MaxADSspace A) by Th32; :: thesis: verum