:: deftheorem defines <= FINANCE5:def 1 :
for A being non empty set
for I being ext-real-membered set
for k1, k2 being Function of A,I holds
( k1 <= k2 iff for w being Element of A holds k1 . w <= k2 . w );