:: deftheorem Def1 defines subadditive HAHNBAN:def 1 :
for V being RealLinearSpace
for IT being Functional of V holds
( IT is subadditive iff for x, y being VECTOR of V holds IT . (x + y) <= (IT . x) + (IT . y) );