let T be non empty TopSpace; :: thesis: ( T is T_2 implies for S being sequence of T st S is convergent holds
ex x being Point of T st Lim S = {x} )
assume A1: T is T_2 ; :: thesis: for S being sequence of T st S is convergent holds
ex x being Point of T st Lim S = {x}
let S be sequence of T; :: thesis: ( S is convergent implies ex x being Point of T st Lim S = {x} )
assume S is convergent ; :: thesis: ex x being Point of T st Lim S = {x}
then consider x being Point of T such that
A2: S is_convergent_to x ;
take x ; :: thesis: Lim S = {x}
A3: x in Lim S by A2, FRECHET:def 5;
thus Lim S c= {x} :: according to XBOOLE_0:def 10 :: thesis: {x} c= Lim S

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Lim S or y in {x} )
assume A4: y in Lim S ; :: thesis: y in {x}
then reconsider y9 = y as Point of T ;
y9 = x by A1, A3, A4, Th6;
hence y in {x} by TARSKI:def 1; :: thesis: verum

end;

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in {x} or y in Lim S )
assume y in {x} ; :: thesis: y in Lim S
hence y in Lim S by A3, TARSKI:def 1; :: thesis: verum