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

proof

let x be set ; :: according to MMLQUER2:def 2 :: thesis: for y being set st x,y in value_of (O,R1) & y,x in value_of (O,R1) holds
x = y
let y be set ; :: thesis: ( x,y in value_of (O,R1) & y,x in value_of (O,R1) implies x = y )
assume A1: ( x,y in value_of (O,R1) & y,x in value_of (O,R1) ) ; :: thesis: x = y
then reconsider x = x, y = y as Element of X by Th2;
( y = y & x = x ) ;
then ( x . O <> {} & ( y . O = {} or ( y . O <> {} & (order ((x . O),R1)) /. 0,(order ((y . O),R1)) /. 0 in R1 & (order ((x . O),R1)) /. 0 <> (order ((y . O),R1)) /. 0 ) ) & y . O <> {} & ( x . O = {} or ( x . O <> {} & (order ((y . O),R1)) /. 0,(order ((x . O),R1)) /. 0 in R1 & (order ((y . O),R1)) /. 0 <> (order ((x . O),R1)) /. 0 ) ) ) by A1, Def12;
hence x = y by Def2; :: thesis: verum

end;

thus value_of (O,R1) is transitive :: thesis: value_of (O,R1) 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 (O,R1) & y,z in value_of (O,R1) holds
x,z in value_of (O,R1)
let y, z be set ; :: thesis: ( x,y in value_of (O,R1) & y,z in value_of (O,R1) implies x,z in value_of (O,R1) )
assume A2: ( x,y in value_of (O,R1) & y,z in value_of (O,R1) ) ; :: thesis: x,z in value_of (O,R1)
then reconsider x = x, y = y, z = z as Element of X by Th2;
( y = y & z = z ) ;
then ( x . O <> {} & ( y . O = {} or ( y . O <> {} & (order ((x . O),R1)) /. 0,(order ((y . O),R1)) /. 0 in R1 & (order ((x . O),R1)) /. 0 <> (order ((y . O),R1)) /. 0 ) ) & y . O <> {} & ( z . O = {} or ( z . O <> {} & (order ((y . O),R1)) /. 0,(order ((z . O),R1)) /. 0 in R1 & (order ((y . O),R1)) /. 0 <> (order ((z . O),R1)) /. 0 ) ) ) by A2, Def12;
then ( x . O <> {} & ( z . O = {} or ( z . O <> {} & (order ((x . O),R1)) /. 0,(order ((z . O),R1)) /. 0 in R1 & (order ((x . O),R1)) /. 0 <> (order ((z . O),R1)) /. 0 ) ) ) by Def1, Def2;
hence x,z in value_of (O,R1) by Def12; :: thesis: verum

end;

let x, y be Element of X; :: according to MMLQUER2:def 4 :: thesis: ( x,y nin value_of (O,R1) implies for z being Element of X st x,z in value_of (O,R1) holds
y,z in value_of (O,R1) )
assume A3: x,y nin value_of (O,R1) ; :: thesis: for z being Element of X st x,z in value_of (O,R1) holds
y,z in value_of (O,R1)
let z be Element of X; :: thesis: ( x,z in value_of (O,R1) implies y,z in value_of (O,R1) )
assume x,z in value_of (O,R1) ; :: thesis: y,z in value_of (O,R1)
then ( x in X & z in X & x . O <> {} & ( z . O = {} or ( z . O <> {} & (order ((x . O),R1)) /. 0,(order ((z . O),R1)) /. 0 in R1 & (order ((x . O),R1)) /. 0 <> (order ((z . O),R1)) /. 0 ) ) & ( x . O = {} or ( y . O <> {} & ( y . O = {} or (order ((x . O),R1)) /. 0,(order ((y . O),R1)) /. 0 nin R1 or (order ((x . O),R1)) /. 0 = (order ((y . O),R1)) /. 0 ) ) ) ) by A3, Th2, Def12;
then ( y . O <> {} & ( z . O = {} or ( z . O <> {} & (order ((y . O),R1)) /. 0,(order ((z . O),R1)) /. 0 in R1 & (order ((y . O),R1)) /. 0 <> (order ((z . O),R1)) /. 0 ) ) ) by Def4;
hence y,z in value_of (O,R1) by Def12; :: thesis: verum