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

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