thus
clf F is discrete
:: thesis: verumproof
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 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 3;
assume that A7:
O meets A
and A8:
O meets B
;
:: thesis: A = Bconsider D being
Subset of
T such that A9:
B = Cl D
and A10:
D in F
by A4, PCOMPS_1:def 3;
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;