for Y being non empty TopStruct
for A being Subset of Y
for x being Point of Y st MaxADSet x meets MaxADSet A holds
MaxADSet x c= MaxADSet A