let X be RealNormSpace; :: thesis: for Y, Z being SubRealNormSpace of X st ex A being Subset of X st
( A = the carrier of Y & Cl A = the carrier of Z ) holds
for D0 being Subset of Y
for D being Subset of Z st D0 is dense & D0 = D holds
D is dense

let Y, Z be SubRealNormSpace of X; :: thesis: ( ex A being Subset of X st
( A = the carrier of Y & Cl A = the carrier of Z ) implies for D0 being Subset of Y
for D being Subset of Z st D0 is dense & D0 = D holds
D is dense )

given A being Subset of X such that A1: ( A = the carrier of Y & Cl A = the carrier of Z ) ; :: thesis: for D0 being Subset of Y
for D being Subset of Z st D0 is dense & D0 = D holds
D is dense

let D0 be Subset of Y; :: thesis: for D being Subset of Z st D0 is dense & D0 = D holds
D is dense

let D be Subset of Z; :: thesis: ( D0 is dense & D0 = D implies D is dense )
assume A2: ( D0 is dense & D0 = D ) ; :: thesis: D is dense
A3: ( the carrier of = the carrier of Z & the carrier of = the carrier of Y & the carrier of = the carrier of X ) by NORMSP_2:def 4;
A4: ( LinearTopSpaceNorm Z is SubSpace of LinearTopSpaceNorm X & LinearTopSpaceNorm Y is SubSpace of LinearTopSpaceNorm X ) by Th2;
for S being Subset of Z st S <> {} & S is open holds
D meets S
proof
let S be Subset of Z; :: thesis: ( S <> {} & S is open implies D meets S )
assume A5: ( S <> {} & S is open ) ; :: thesis: D meets S
reconsider SZL = S as Subset of by NORMSP_2:def 4;
reconsider SZT = SZL as Subset of () ;
SZT is open by ;
then SZL is open by NORMSP_2:20;
then consider SXL being Subset of such that
A6: ( SXL in the topology of & SZL = SXL /\ () ) by ;
reconsider SYL = SXL /\ () as Subset of ;
reconsider SX = SXL as Subset of X by NORMSP_2:def 4;
reconsider SXT = SXL as Subset of () by NORMSP_2:def 4;
reconsider SY = SYL as Subset of Y by NORMSP_2:def 4;
reconsider SYT = SYL as Subset of () by NORMSP_2:def 4;
SXL is open by A6;
then SXT is open by NORMSP_2:20;
then A7: SX is open by NORMSP_2:16;
SX /\ (Cl A) <> {} by ;
then consider v being object such that
A8: v in SX /\ (Cl A) by XBOOLE_0:def 1;
( v in SX & v in Cl A ) by ;
then SX meets A by ;
then A9: SYL <> {} by ;
SYL is open by ;
then SYT is open by NORMSP_2:20;
then SY is open by NORMSP_2:16;
then A10: D0 meets SY by ;
SYL c= SZL by ;
then D /\ SYL c= D /\ SZL by XBOOLE_1:26;
hence D meets S by ; :: thesis: verum
end;
hence D is dense by NORMSP_3:17; :: thesis: verum