theorem Th3: :: NORMSP_4:3

for X being RealNormSpace
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