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