thus clf F is discrete :: thesis: verum
proof
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 clf F & B in clf F & O meets A & O meets B holds
A = B ) )

consider O being open Subset of T such that
A1: p in O and
A2: for A, B being Subset of T st A in F & B in F & O meets A & O meets B holds
A = B by Def1;
now :: thesis: for A, B being Subset of T st A in clf F & B in clf F & O meets A & O meets B holds
A = B
let A, B be Subset of T; :: thesis: ( A in clf F & B in clf F & O meets A & O meets B implies A = B )
assume that
A3: A in clf F and
A4: B in clf F ; :: thesis: ( O meets A & O meets B implies A = B )
consider C being Subset of T such that
A5: A = Cl C and
A6: C in F by ;
assume that
A7: O meets A and
A8: O meets B ; :: thesis: A = B
consider D being Subset of T such that
A9: B = Cl D and
A10: D in F by ;
A11: O meets D by A9, A8, Lm3;
O meets C by A5, A7, Lm3;
hence A = B by A2, A5, A6, A9, A10, A11; :: thesis: verum
end;
hence ex O being open Subset of T st
( p in O & ( for A, B being Subset of T st A in clf F & B in clf F & O meets A & O meets B holds
A = B ) ) by A1; :: thesis: verum
end;