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

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