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 )