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;
hereby :: thesis: ( ( 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
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;
end;
assume A3: for S being Subset of X st S <> {} & S is open holds
R meets S ; :: thesis: R is dense
for S1 being Subset of (LinearTopSpaceNorm X) st S1 <> {} & S1 is open holds
R1 meets S1
proof
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;
then R1 is dense by TOPS_1:45;
hence R is dense by EQCL2; :: thesis: verum