reconsider F = {} as Subset-Family of T by XBOOLE_1:2;

take F ; :: thesis: ( F is empty & F is discrete )

thus F is empty ; :: 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 [#] T ; :: thesis: ( p in [#] T & ( for A, B being Subset of T st A in F & B in F & [#] T meets A & [#] T meets B holds

A = B ) )

thus ( p in [#] T & ( for A, B being Subset of T st A in F & B in F & [#] T meets A & [#] T meets B holds

A = B ) ) ; :: thesis: verum

take F ; :: thesis: ( F is empty & F is discrete )

thus F is empty ; :: 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 [#] T ; :: thesis: ( p in [#] T & ( for A, B being Subset of T st A in F & B in F & [#] T meets A & [#] T meets B holds

A = B ) )

thus ( p in [#] T & ( for A, B being Subset of T st A in F & B in F & [#] T meets A & [#] T meets B holds

A = B ) ) ; :: thesis: verum