theorem NONEMP: :: NORMSP_3:20

for X being RealNormSpace
for A being Subset of X st A is dense holds
not A is empty