:: deftheorem defines <= YELLOW_2:def 1 :
for J being set
for L being RelStr
for f, g being Function of J, the carrier of L holds
( f <= g iff for j being set st j in J holds
ex a, b being Element of L st
( a = f . j & b = g . j & a <= b ) );