:: deftheorem defines <= COUSIN2:def 3 :
for X being non empty set
for f, g being Function of X,REAL holds
( f <= g iff for x being Element of X holds f . x <= g . x );