:: deftheorem defines MaxADSet TEX_4:def 8 :
for Y being TopStruct
for x being Point of Y holds MaxADSet x = union (MaxADSF x);