let X be RealUnitarySpace; :: thesis: for Y being Subset of X holds
( Y is closed iff for s being sequence of X st rng s c= Y & s is convergent holds
lim s in Y )

let Y be Subset of X; :: thesis: ( Y is closed iff for s being sequence of X st rng s c= Y & s is convergent holds
lim s in Y )

hereby :: thesis: ( ( for s being sequence of X st rng s c= Y & s is convergent holds
lim s in Y ) implies Y is closed )
assume Y is closed ; :: thesis: for s being sequence of X st rng s c= Y & s is convergent holds
lim s in Y

then consider Z being Subset of () such that
A1: ( Z = Y & Z is closed ) ;
thus for s being sequence of X st rng s c= Y & s is convergent holds
lim s in Y :: thesis: verum
proof
let s be sequence of X; :: thesis: ( rng s c= Y & s is convergent implies lim s in Y )
assume A3: ( rng s c= Y & s is convergent ) ; :: thesis: lim s in Y
reconsider s1 = s as sequence of () ;
( rng s1 c= Z & s1 is convergent ) by A3, A1, RHS8;
then lim s1 in Z by A1;
hence lim s in Y by A1, A3, RHS9; :: thesis: verum
end;
end;
assume A4: for s being sequence of X st rng s c= Y & s is convergent holds
lim s in Y ; :: thesis: Y is closed
reconsider Z = Y as Subset of () ;
for s1 being sequence of () st rng s1 c= Z & s1 is convergent holds
lim s1 in Z
proof
let s1 be sequence of (); :: thesis: ( rng s1 c= Z & s1 is convergent implies lim s1 in Z )
assume A5: ( rng s1 c= Z & s1 is convergent ) ; :: thesis: lim s1 in Z
reconsider s = s1 as sequence of X ;
A6: ( rng s c= Y & s is convergent ) by ;
then lim s in Y by A4;
hence lim s1 in Z by ; :: thesis: verum
end;
then Z is closed ;
hence Y is closed ; :: thesis: verum