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;

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

then v in Cl Z by A5, PRE_TOPC:def 7;

hence v in Cl Y by EQCL1; :: thesis: verum

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 A4:
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

end;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;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

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

v in the carrier of (LinearTopSpaceNorm X)
by A1, NORMSP_2:def 4;
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;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

then v in Cl Z by A5, PRE_TOPC:def 7;

hence v in Cl Y by EQCL1; :: thesis: verum