let T be non empty TopSpace; :: thesis: ( not T is T_1 implies ex x1, x2 being Point of T ex S being sequence of T st
( S = NAT --> x1 & x1 <> x2 & S is_convergent_to x2 ) )
assume not T is T_1 ; :: thesis: ex x1, x2 being Point of T ex S being sequence of T st
( S = NAT --> x1 & x1 <> x2 & S is_convergent_to x2 )
then consider x1, x2 being Point of T such that
A1: x1 <> x2 and
A2: x2 in Cl {x1} by Lm2;
set S = NAT --> x1;
take x1 ; :: thesis: ex x2 being Point of T ex S being sequence of T st
( S = NAT --> x1 & x1 <> x2 & S is_convergent_to x2 )
take x2 ; :: thesis: ex S being sequence of T st
( S = NAT --> x1 & x1 <> x2 & S is_convergent_to x2 )
take NAT --> x1 ; :: thesis: ( NAT --> x1 = NAT --> x1 & x1 <> x2 & NAT --> x1 is_convergent_to x2 )
thus NAT --> x1 = NAT --> x1 ; :: thesis: ( x1 <> x2 & NAT --> x1 is_convergent_to x2 )
thus x1 <> x2 by A1; :: thesis: NAT --> x1 is_convergent_to x2
thus NAT --> x1 is_convergent_to x2 :: thesis: verum

proof

let U1 be Subset of T; :: according to FRECHET:def 3 :: thesis: ( not U1 is open or not x2 in U1 or ex b₁ being set st
for b₂ being set holds
( not b₁ <= b₂ or (NAT --> x1) . b₂ in U1 ) )
assume A3: ( U1 is open & x2 in U1 ) ; :: thesis: ex b₁ being set st
for b₂ being set holds
( not b₁ <= b₂ or (NAT --> x1) . b₂ in U1 )
take 0 ; :: thesis: for b₁ being set holds
( not 0 <= b₁ or (NAT --> x1) . b₁ in U1 )
let n be Nat; :: thesis: ( not 0 <= n or (NAT --> x1) . n in U1 )
A4: n in NAT by ORDINAL1:def 12;
assume 0 <= n ; :: thesis: (NAT --> x1) . n in U1
{x1} meets U1 by A2, A3, PRE_TOPC:def 7;
then x1 in U1 by ZFMISC_1:50;
hence (NAT --> x1) . n in U1 by FUNCOP_1:7, A4; :: thesis: verum

end;