let T be non empty TopSpace; :: thesis: ( T is first-countable implies ( T is T_2 iff for S being sequence of T
for x1, x2 being Point of T st x1 in Lim S & x2 in Lim S holds
x1 = x2 ) )
assume A1:
T is first-countable
; :: thesis: ( T is T_2 iff for S being sequence of T
for x1, x2 being Point of T st x1 in Lim S & x2 in Lim S holds
x1 = x2 )
thus
( T is T_2 implies for S being sequence of T
for x1, x2 being Point of T st x1 in Lim S & x2 in Lim S holds
x1 = x2 )
by Th9; :: thesis: ( ( for S being sequence of T
for x1, x2 being Point of T st x1 in Lim S & x2 in Lim S holds
x1 = x2 ) implies T is T_2 )
assume A2:
for S being sequence of T
for x1, x2 being Point of T st x1 in Lim S & x2 in Lim S holds
x1 = x2
; :: thesis: T is T_2
assume
not T is T_2
; :: thesis: contradiction
then consider x1, x2 being Point of T such that
A3:
x1 <> x2
and
A4:
for U1, U2 being Subset of T st U1 is open & U2 is open & x1 in U1 & x2 in U2 holds
U1 meets U2
by PRE_TOPC:def 16;
consider B1 being Basis of x1 such that
A5:
ex S being Function st
( dom S = NAT & rng S = B1 & ( for n, m being Element of NAT st m >= n holds
S . m c= S . n ) )
by A1, Lm10;
consider S1 being Function such that
A6:
dom S1 = NAT
and
A7:
rng S1 = B1
and
A8:
for n, m being Element of NAT st m >= n holds
S1 . m c= S1 . n
by A5;
consider B2 being Basis of x2 such that
A9:
ex S being Function st
( dom S = NAT & rng S = B2 & ( for n, m being Element of NAT st m >= n holds
S . m c= S . n ) )
by A1, Lm10;
consider S2 being Function such that
A10:
dom S2 = NAT
and
A11:
rng S2 = B2
and
A12:
for n, m being Element of NAT st m >= n holds
S2 . m c= S2 . n
by A9;
defpred S1[ set , set ] means $2 in (S1 . $1) /\ (S2 . $1);
A13:
for n being set st n in NAT holds
ex x being set st
( x in the carrier of T & S1[n,x] )
proof
let n be
set ;
:: thesis: ( n in NAT implies ex x being set st
( x in the carrier of T & S1[n,x] ) )
assume A14:
n in NAT
;
:: thesis: ex x being set st
( x in the carrier of T & S1[n,x] )
then A15:
S1 . n in B1
by A6, A7, FUNCT_1:def 5;
then reconsider U1 =
S1 . n as
Subset of
T ;
reconsider U1 =
U1 as
Subset of
T ;
A16:
(
U1 is
open &
x1 in U1 )
by A15, YELLOW_8:21;
A17:
S2 . n in B2
by A10, A11, A14, FUNCT_1:def 5;
then reconsider U2 =
S2 . n as
Subset of
T ;
reconsider U2 =
U2 as
Subset of
T ;
(
U2 is
open &
x2 in U2 )
by A17, YELLOW_8:21;
then
U1 meets U2
by A4, A16;
then A18:
U1 /\ U2 <> {}
by XBOOLE_0:def 7;
consider x being
Element of
(S1 . n) /\ (S2 . n);
take
x
;
:: thesis: ( x in the carrier of T & S1[n,x] )
x in U1 /\ U2
by A18;
hence
x in the
carrier of
T
;
:: thesis: S1[n,x]
thus
x in (S1 . n) /\ (S2 . n)
by A18;
:: thesis: verum
end;
consider S being Function such that
A19:
dom S = NAT
and
A20:
rng S c= the carrier of T
and
A21:
for n being set st n in NAT holds
S1[n,S . n]
from WELLORD2:sch 1(A13);
reconsider S = S as Function of NAT ,the carrier of T by A19, A20, FUNCT_2:def 1, RELSET_1:11;
S is_convergent_to x1
then A28:
x1 in Lim S
by FRECHET:def 4;
S is_convergent_to x2
then
x2 in Lim S
by FRECHET:def 4;
hence
contradiction
by A2, A3, A28; :: thesis: verum