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

proof

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;

then [#] X c= Cl A ;
then [#] X = Cl A ;
hence A is dense ; :: thesis: verum