theorem TOPS145: :: NORMSP_3:17

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