let X be finite set ; :: thesis: 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) )
let O be Operation of X; :: thesis: for x, y being Element of X holds
( x,y in value_of (number_of O) iff card (x . O) < card (y . O) )
let x, y be Element of X; :: thesis: ( x,y in value_of (number_of O) iff card (x . O) < card (y . O) )

hereby :: thesis: ( card (x . O) < card (y . O) implies x,y in value_of (number_of O) )

assume x,y in value_of (number_of O) ; :: thesis: card (x . O) < card (y . O)
then (number_of O) . x < (number_of O) . y by Def5;
then card (x . O) < (number_of O) . y by Def6;
hence card (x . O) < card (y . O) by Def6; :: thesis: verum

end;

assume A1: card (x . O) < card (y . O) ; :: thesis: x,y in value_of (number_of O)
0 <= card (x . O) by NAT_1:2;
then y . O <> {} by A1;
then ( y in dom O & (number_of O) . x = card (x . O) & (number_of O) . y = card (y . O) ) by Def6, RELAT_1:170;
hence x,y in value_of (number_of O) by A1, Def5; :: thesis: verum