set F = { A where A is Subset of Y : ( A is anti-discrete & x in A ) } ;
{ A where A is Subset of Y : ( A is anti-discrete & x in A ) } c= bool the carrier of Y

proof

let C be object ; :: according to TARSKI:def 3 :: thesis: ( not C in { A where A is Subset of Y : ( A is anti-discrete & x in A ) } or C in bool the carrier of Y )
assume C in { A where A is Subset of Y : ( A is anti-discrete & x in A ) } ; :: thesis: C in bool the carrier of Y
then ex A being Subset of Y st
( C = A & A is anti-discrete & x in A ) ;
hence C in bool the carrier of Y ; :: thesis: verum

end;

hence { A where A is Subset of Y : ( A is anti-discrete & x in A ) } is Subset-Family of Y ; :: thesis: verum