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 & ( 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

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 A2: ( A in clf F & B in clf F ) ; :: thesis: ( O meets A & O meets B implies A = B )
then consider C being Subset of T such that
A3: ( A = Cl C & C in F ) by PCOMPS_1:def 3;
consider D being Subset of T such that
A4: ( B = Cl D & D in F ) by A2, PCOMPS_1:def 3;
assume ( O meets A & O meets B ) ; :: thesis: A = B
then ( O meets C & O meets D & C in F & D in F ) by A3, A4, Lm3;
hence A = B by A1, A3, A4; :: 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;