now :: thesis: MaxADSet A is empty

assume not MaxADSet A is empty ; :: thesis: contradiction
then consider x being object such that
A1: x in MaxADSet A ;
reconsider a = x as Point of Y by A1;
consider D being set such that
a in D and
A2: D in { (MaxADSet b) where b is Point of Y : b in A } by A1, TARSKI:def 4;
ex b being Point of Y st
( D = MaxADSet b & b in A ) by A2;
hence contradiction ; :: thesis: verum

end;

hence MaxADSet A is empty ; :: thesis: verum