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