set R = value_of f;
thus value_of f is antisymmetric :: thesis: ( value_of f is transitive & value_of f is beta-transitive )

proof

let x be set ; :: according to MMLQUER2:def 2 :: thesis: for y being set st x,y in value_of f & y,x in value_of f holds
x = y
let y be set ; :: thesis: ( x,y in value_of f & y,x in value_of f implies x = y )
assume ( x,y in value_of f & y,x in value_of f ) ; :: thesis: x = y
then ( f . x < f . y & f . y < f . x ) by Def5;
hence x = y ; :: thesis: verum

end;

thus value_of f is transitive :: thesis: value_of f is beta-transitive

proof

let x be set ; :: according to MMLQUER2:def 1 :: thesis: for y, z being set st x,y in value_of f & y,z in value_of f holds
x,z in value_of f
let y, z be set ; :: thesis: ( x,y in value_of f & y,z in value_of f implies x,z in value_of f )
assume ( x,y in value_of f & y,z in value_of f ) ; :: thesis: x,z in value_of f
then A1: ( x in X & z in X & f . x < f . y & f . y < f . z ) by Def5;
then f . x < f . z by XXREAL_0:2;
hence x,z in value_of f by A1, Def5; :: thesis: verum

end;

let x, y be Element of X; :: according to MMLQUER2:def 4 :: thesis: ( x,y nin value_of f implies for z being Element of X st x,z in value_of f holds
y,z in value_of f )
assume A2: x,y nin value_of f ; :: thesis: for z being Element of X st x,z in value_of f holds
y,z in value_of f
let z be Element of X; :: thesis: ( x,z in value_of f implies y,z in value_of f )
assume x,z in value_of f ; :: thesis: y,z in value_of f
then A3: ( x in X & f . x < f . z ) by Def5;
then f . x >= f . y by A2, Def5;
then f . y < f . z by A3, XXREAL_0:2;
hence y,z in value_of f by A3, Def5; :: thesis: verum