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;

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

hence
ex O being open Subset of T st 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 A3, PCOMPS_1:def 2;

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 A4, PCOMPS_1:def 2;

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;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 A3, PCOMPS_1:def 2;

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 A4, PCOMPS_1:def 2;

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

( 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