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