now :: thesis: MaxADSet A is empty

hence
MaxADSet A is empty
; :: thesis: verumassume
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;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