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

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

proof

hence
{ A where A is Subset of Y : ( A is anti-discrete & x in A ) } is Subset-Family of Y
; :: thesis: verum
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;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