let X be RealNormSpace; :: thesis: for Y being Subset of X
for v being object st v in the carrier of X holds
( v in Cl Y iff for G being Subset of X st G is open & v in G holds
G meets Y )

let Y be Subset of X; :: thesis: for v being object st v in the carrier of X holds
( v in Cl Y iff for G being Subset of X st G is open & v in G holds
G meets Y )

let v be object ; :: thesis: ( v in the carrier of X implies ( v in Cl Y iff for G being Subset of X st G is open & v in G holds
G meets Y ) )

assume A1: v in the carrier of X ; :: thesis: ( v in Cl Y iff for G being Subset of X st G is open & v in G holds
G meets Y )

reconsider Z = Y as Subset of by NORMSP_2:def 4;
hereby :: thesis: ( ( for G being Subset of X st G is open & v in G holds
G meets Y ) implies v in Cl Y )
assume v in Cl Y ; :: thesis: for G being Subset of X st G is open & v in G holds
G meets Y

then A2: v in Cl Z by EQCL1;
thus for G being Subset of X st G is open & v in G holds
G meets Y :: thesis: verum
proof
let G be Subset of X; :: thesis: ( G is open & v in G implies G meets Y )
assume A3: ( G is open & v in G ) ; :: thesis: G meets Y
reconsider G0 = G as Subset of by NORMSP_2:def 4;
G0 is open by ;
hence G meets Y by ; :: thesis: verum
end;
end;
assume A4: for G being Subset of X st G is open & v in G holds
G meets Y ; :: thesis: v in Cl Y
A5: for G0 being Subset of st G0 is open & v in G0 holds
G0 meets Z
proof
let G0 be Subset of ; :: thesis: ( G0 is open & v in G0 implies G0 meets Z )
assume A6: ( G0 is open & v in G0 ) ; :: thesis: G0 meets Z
reconsider G = G0 as Subset of X by NORMSP_2:def 4;
G is open by ;
hence G0 meets Z by A4, A6; :: thesis: verum
end;
v in the carrier of by ;
then v in Cl Z by ;
hence v in Cl Y by EQCL1; :: thesis: verum