:: deftheorem Def12 defines value_of MMLQUER2:def 12 :
for X being finite set
for O being Operation of X
for R being connected Order of X
for b₄ being Relation of X holds
( b₄ = value_of (O,R) iff for x, y being Element of X holds
( x,y in b₄ iff ( x . O <> {} & ( y . O = {} or ( y . O <> {} & (order ((x . O),R)) /. 0,(order ((y . O),R)) /. 0 in R & (order ((x . O),R)) /. 0 <> (order ((y . O),R)) /. 0 ) ) ) ) );