:: deftheorem Def7 defines first MMLQUER2:def 7 :
for X being set
for O being Operation of X
for b₃ being Relation of X holds
( b₃ = first O iff for x, y being Element of X holds
( x,y in b₃ iff ( x . O <> {} & y . O = {} ) ) );