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
proof
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;
hence { x where x is Subset of T : ( x is open & x is closed ) } is Subset-Family of T ; :: thesis: verum