for Y being non empty TopStruct
for A being non empty Subset of Y holds A is Subset of (MaxADSspace A)