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

( R is dense iff for S being Subset of X st S <> {} & S is open holds

R meets S )

let R be Subset of X; :: thesis: ( R is dense iff for S being Subset of X st S <> {} & S is open holds

R meets S )

reconsider R1 = R as Subset of (LinearTopSpaceNorm X) by NORMSP_2:def 4;

R meets S ; :: thesis: R is dense

for S1 being Subset of (LinearTopSpaceNorm X) st S1 <> {} & S1 is open holds

R1 meets S1

hence R is dense by EQCL2; :: thesis: verum

( R is dense iff for S being Subset of X st S <> {} & S is open holds

R meets S )

let R be Subset of X; :: thesis: ( R is dense iff for S being Subset of X st S <> {} & S is open holds

R meets S )

reconsider R1 = R as Subset of (LinearTopSpaceNorm X) by NORMSP_2:def 4;

hereby :: thesis: ( ( for S being Subset of X st S <> {} & S is open holds

R meets S ) implies R is dense )

assume A3:
for S being Subset of X st S <> {} & S is open holds R meets S ) implies R is dense )

assume
R is dense
; :: thesis: for S being Subset of X st S <> {} & S is open holds

R meets S

then A1: R1 is dense by EQCL2;

thus for S being Subset of X st S <> {} & S is open holds

R meets S :: thesis: verum

end;R meets S

then A1: R1 is dense by EQCL2;

thus for S being Subset of X st S <> {} & S is open holds

R meets S :: thesis: verum

proof

let S be Subset of X; :: thesis: ( S <> {} & S is open implies R meets S )

assume A2: ( S <> {} & S is open ) ; :: thesis: R meets S

reconsider S1 = S as Subset of (LinearTopSpaceNorm X) by NORMSP_2:def 4;

S1 is open by A2, NORMSP_2:33;

hence R meets S by A1, A2, TOPS_1:45; :: thesis: verum

end;assume A2: ( S <> {} & S is open ) ; :: thesis: R meets S

reconsider S1 = S as Subset of (LinearTopSpaceNorm X) by NORMSP_2:def 4;

S1 is open by A2, NORMSP_2:33;

hence R meets S by A1, A2, TOPS_1:45; :: thesis: verum

R meets S ; :: thesis: R is dense

for S1 being Subset of (LinearTopSpaceNorm X) st S1 <> {} & S1 is open holds

R1 meets S1

proof

then
R1 is dense
by TOPS_1:45;
let S1 be Subset of (LinearTopSpaceNorm X); :: thesis: ( S1 <> {} & S1 is open implies R1 meets S1 )

assume A4: ( S1 <> {} & S1 is open ) ; :: thesis: R1 meets S1

reconsider S = S1 as Subset of X by NORMSP_2:def 4;

S is open by A4, NORMSP_2:33;

hence R1 meets S1 by A3, A4; :: thesis: verum

end;assume A4: ( S1 <> {} & S1 is open ) ; :: thesis: R1 meets S1

reconsider S = S1 as Subset of X by NORMSP_2:def 4;

S is open by A4, NORMSP_2:33;

hence R1 meets S1 by A3, A4; :: thesis: verum

hence R is dense by EQCL2; :: thesis: verum