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 (LinearTopSpaceNorm X) 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 (LinearTopSpaceNorm X) by NORMSP_2:def 4;
G0 is open by A3, NORMSP_2:33;
hence G meets Y by A2, A3, PRE_TOPC:def 7; :: 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 (LinearTopSpaceNorm X) st G0 is open & v in G0 holds
G0 meets Z
proof
let G0 be Subset of (LinearTopSpaceNorm X); :: 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 A6, NORMSP_2:33;
hence G0 meets Z by A4, A6; :: thesis: verum
end;
v in the carrier of (LinearTopSpaceNorm X) by A1, NORMSP_2:def 4;
then v in Cl Z by A5, PRE_TOPC:def 7;
hence v in Cl Y by EQCL1; :: thesis: verum