let T be non empty TopSpace; :: thesis: ( T is T_2 implies for S being sequence of T
for x being Point of T holds
( S is_convergent_to x iff ( S is convergent & x = lim S ) ) )
assume A1: T is T_2 ; :: thesis: for S being sequence of T
for x being Point of T holds
( S is_convergent_to x iff ( S is convergent & x = lim S ) )
let S be sequence of T; :: thesis: for x being Point of T holds
( S is_convergent_to x iff ( S is convergent & x = lim S ) )
let x be Point of T; :: thesis: ( S is_convergent_to x iff ( S is convergent & x = lim S ) )
thus ( S is_convergent_to x implies ( S is convergent & x = lim S ) ) :: thesis: ( S is convergent & x = lim S implies S is_convergent_to x )

proof

assume A2: S is_convergent_to x ; :: thesis: ( S is convergent & x = lim S )
hence S is convergent ; :: thesis: x = lim S
then ex y being Point of T st Lim S = {y} by A1, Th24;
hence x = lim S by A2, Def2; :: thesis: verum

end;

assume that
A3: S is convergent and
A4: x = lim S ; :: thesis: S is_convergent_to x
ex x being Point of T st Lim S = {x} by A1, A3, Th24;
hence S is_convergent_to x by A4, Def2; :: thesis: verum