let T be non empty TopSpace; :: thesis: ( 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 )
assume A1: T is T_2 ; :: 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
assume ex S being sequence of T ex x1, x2 being Point of T st
( x1 in Lim S & x2 in Lim S & not x1 = x2 ) ; :: thesis: contradiction
then consider S being sequence of T such that
A2: ex x1, x2 being Point of T st
( x1 in Lim S & x2 in Lim S & x1 <> x2 ) ;
consider x1, x2 being Point of T such that
A3: x1 in Lim S and
A4: x2 in Lim S and
A5: x1 <> x2 by A2;
consider U1, U2 being Subset of T such that
A6: U1 is open and
A7: U2 is open and
A8: x1 in U1 and
A9: x2 in U2 and
A10: U1 misses U2 by A1, A5;
S is_convergent_to x1 by A3, FRECHET:def 5;
then consider n1 being Nat such that
A11: for m being Nat st n1 <= m holds
S . m in U1 by A6, A8;
S is_convergent_to x2 by A4, FRECHET:def 5;
then consider n2 being Nat such that
A12: for m being Nat st n2 <= m holds
S . m in U2 by A7, A9;
reconsider n = max (n1,n2) as Element of NAT by ORDINAL1:def 12;
A13: S . n in U1 by A11, XXREAL_0:25;
A14: S . n in U2 by A12, XXREAL_0:25;
U1 /\ U2 = {} by A10;
hence contradiction by A13, A14, XBOOLE_0:def 4; :: thesis: verum