set F = {{}, the carrier of T};
{{}, the carrier of T} c= bool the carrier of T

proof

let f be object ; :: according to TARSKI:def 3 :: thesis: ( not f in {{}, the carrier of T} or f in bool the carrier of T )
reconsider ff = f as set by TARSKI:1;
assume f in {{}, the carrier of T} ; :: thesis: f in bool the carrier of T
then ( f = {} or f = the carrier of T ) by TARSKI:def 2;
then ff c= the carrier of T ;
hence f in bool the carrier of T ; :: thesis: verum

end;

then reconsider F = {{}, the carrier of T} as Subset-Family of T ;
take F ; :: thesis: F is discrete
let p be Point of T; :: according to NAGATA_1:def 1 :: thesis: ex O being open Subset of T st
( p in O & ( for A, B being Subset of T st A in F & B in F & O meets A & O meets B holds
A = B ) )
take O = [#] T; :: thesis: ( p in O & ( for A, B being Subset of T st A in F & B in F & O meets A & O meets B holds
A = B ) )
thus p in O ; :: thesis: for A, B being Subset of T st A in F & B in F & O meets A & O meets B holds
A = B

now :: thesis: for A, B being Subset of T st A in F & B in F & O meets A & O meets B holds
A = B

let A, B be Subset of T; :: thesis: ( A in F & B in F & O meets A & O meets B implies A = B )
assume that
A1: A in F and
A2: B in F ; :: thesis: ( O meets A & O meets B implies A = B )
A3: ( B = {} or B = the carrier of T ) by A2, TARSKI:def 2;
assume ( O meets A & O meets B ) ; :: thesis: A = B
then A4: ( O /\ A <> {} & O /\ B <> {} ) by XBOOLE_0:def 7;
( A = {} or A = the carrier of T ) by A1, TARSKI:def 2;
hence A = B by A3, A4; :: thesis: verum

end;

hence for A, B being Subset of T st A in F & B in F & O meets A & O meets B holds
A = B ; :: thesis: verum