for Y being non empty TopStruct
for x, y being Point of Y holds
( MaxADSet x misses MaxADSet y or MaxADSet x = MaxADSet y )