:: deftheorem defines <=_ ARROW:def 4 :
for o being Relation
for a, b being set holds
( a <=_ o,b iff [a,b] in o );