set F = { A where A is Subset of Y : ( A is anti-discrete & x in A ) } ;
( {x} is anti-discrete & x in {x} ) by Th8, TARSKI:def 1;
then {x} in { A where A is Subset of Y : ( A is anti-discrete & x in A ) } ;
hence not MaxADSF x is empty ; :: thesis: verum