theorem :: MMLQUER2:14

for X being finite set
for O being Operation of X
for x, y being Element of X holds
( x,y in value_of (number_of O) iff card (x . O) < card (y . O) )