set A = { x where x is Subset of T : ( x is open & x is closed ) } ;

{ x where x is Subset of T : ( x is open & x is closed ) } c= bool the carrier of T

{ x where x is Subset of T : ( x is open & x is closed ) } c= bool the carrier of T

proof

hence
{ x where x is Subset of T : ( x is open & x is closed ) } is Subset-Family of T
; :: thesis: verum
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { x where x is Subset of T : ( x is open & x is closed ) } or y in bool the carrier of T )

assume y in { x where x is Subset of T : ( x is open & x is closed ) } ; :: thesis: y in bool the carrier of T

then ex x being Subset of T st

( y = x & x is open & x is closed ) ;

hence y in bool the carrier of T ; :: thesis: verum

end;assume y in { x where x is Subset of T : ( x is open & x is closed ) } ; :: thesis: y in bool the carrier of T

then ex x being Subset of T st

( y = x & x is open & x is closed ) ;

hence y in bool the carrier of T ; :: thesis: verum