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

{{}, the carrier of T} c= bool the carrier 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

A = B ; :: thesis: verum

{{}, the carrier of T} c= bool the carrier of T

proof

then reconsider F = {{}, the carrier of T} as Subset-Family of T ;
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;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

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

hence
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;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

A = B ; :: thesis: verum