thus
clf F is discrete
verumproof
let p be
Point of
T;
NAGATA_1:def 1 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 for A, B being Subset of T st A in clf F & B in clf F & O meets A & O meets B holds
A = Blet A,
B be
Subset of
T;
( 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
;
( 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
;
A = Bconsider 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;
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;
verum
end;