set R = value_of (O,R1);
thus
value_of (O,R1) is antisymmetric
( value_of (O,R1) is transitive & value_of (O,R1) is beta-transitive )proof
let x be
set ;
MMLQUER2:def 2 for y being set st x,y in value_of (O,R1) & y,x in value_of (O,R1) holds
x = ylet y be
set ;
( 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) )
;
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;
verum
end;
thus
value_of (O,R1) is transitive
value_of (O,R1) is beta-transitive proof
let x be
set ;
MMLQUER2:def 1 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 ;
( 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) )
;
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;
verum
end;
let x, y be Element of X; MMLQUER2:def 4 ( 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)
; 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; ( x,z in value_of (O,R1) implies y,z in value_of (O,R1) )
assume
x,z in value_of (O,R1)
; 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; verum