:: deftheorem Def1 defines RealNormSpace-like NORMSP_1:def 1 :
for IT being non empty NORMSTR holds
( IT is RealNormSpace-like iff for x, y being Point of IT
for a being Real holds
( ||.(a * x).|| = |.a.| * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| ) );