let X be RealNormSpace; :: thesis: for A being Subset of X holds

( A is dense iff for x being Point of X ex seq being sequence of X st

( rng seq c= A & seq is convergent & lim seq = x ) )

let A be Subset of X; :: thesis: ( A is dense iff for x being Point of X ex seq being sequence of X st

( rng seq c= A & seq is convergent & lim seq = x ) )

thus ( A is dense implies for x being Point of X ex seq being sequence of X st

( rng seq c= A & seq is convergent & lim seq = x ) ) by EQCL3; :: thesis: ( ( for x being Point of X ex seq being sequence of X st

( rng seq c= A & seq is convergent & lim seq = x ) ) implies A is dense )

assume A1: for x being Point of X ex seq being sequence of X st

( rng seq c= A & seq is convergent & lim seq = x ) ; :: thesis: A is dense

for z being object st z in [#] X holds

z in Cl A

then [#] X = Cl A ;

hence A is dense ; :: thesis: verum

( A is dense iff for x being Point of X ex seq being sequence of X st

( rng seq c= A & seq is convergent & lim seq = x ) )

let A be Subset of X; :: thesis: ( A is dense iff for x being Point of X ex seq being sequence of X st

( rng seq c= A & seq is convergent & lim seq = x ) )

thus ( A is dense implies for x being Point of X ex seq being sequence of X st

( rng seq c= A & seq is convergent & lim seq = x ) ) by EQCL3; :: thesis: ( ( for x being Point of X ex seq being sequence of X st

( rng seq c= A & seq is convergent & lim seq = x ) ) implies A is dense )

assume A1: for x being Point of X ex seq being sequence of X st

( rng seq c= A & seq is convergent & lim seq = x ) ; :: thesis: A is dense

for z being object st z in [#] X holds

z in Cl A

proof

then
[#] X c= Cl A
;
let z be object ; :: thesis: ( z in [#] X implies z in Cl A )

assume z in [#] X ; :: thesis: z in Cl A

then reconsider x = z as Point of X ;

ex seq being sequence of X st

( rng seq c= A & seq is convergent & lim seq = x ) by A1;

hence z in Cl A by EQCL3; :: thesis: verum

end;assume z in [#] X ; :: thesis: z in Cl A

then reconsider x = z as Point of X ;

ex seq being sequence of X st

( rng seq c= A & seq is convergent & lim seq = x ) by A1;

hence z in Cl A by EQCL3; :: thesis: verum

then [#] X = Cl A ;

hence A is dense ; :: thesis: verum