set DM = DershowitzMannaOrder R;
thus DershowitzMannaOrder R is asymmetric :: thesis: DershowitzMannaOrder R is transitive

proof

let a be object ; :: according to RELAT_2:def 5,OPOSET_1:def 9 :: thesis: for b₁ being object holds
( not a in the carrier of (DershowitzMannaOrder R) or not b₁ in the carrier of (DershowitzMannaOrder R) or not [a,b₁] in the InternalRel of (DershowitzMannaOrder R) or not [b₁,a] in the InternalRel of (DershowitzMannaOrder R) )
let b be object ; :: thesis: ( not a in the carrier of (DershowitzMannaOrder R) or not b in the carrier of (DershowitzMannaOrder R) or not [a,b] in the InternalRel of (DershowitzMannaOrder R) or not [b,a] in the InternalRel of (DershowitzMannaOrder R) )
assume ( a in the carrier of (DershowitzMannaOrder R) & b in the carrier of (DershowitzMannaOrder R) ) ; :: thesis: ( not [a,b] in the InternalRel of (DershowitzMannaOrder R) or not [b,a] in the InternalRel of (DershowitzMannaOrder R) )
then reconsider m = a, n = b as Element of (DershowitzMannaOrder R) ;
assume ( [a,b] in the InternalRel of (DershowitzMannaOrder R) & [b,a] in the InternalRel of (DershowitzMannaOrder R) ) ; :: thesis: contradiction
then A0: ( m <= n & n <= m ) by ORDERS_2:def 5;
then ( m <> n & ( for a being Element of R st m . a > n . a holds
ex b being Element of R st
( a <= b & m . b < n . b ) ) & ( for a being Element of R st n . a > m . a holds
ex b being Element of R st
( a <= b & n . b < m . b ) ) ) by HO;
then consider c being object such that
A2: ( c in the carrier of R & m . c <> n . c ) by PBOOLE:def 10;
reconsider c = c as Element of R by A2;
set X = { d where d is Element of R : ( c <= d & m . d > n . d ) } ;
BC: { d where d is Element of R : ( c <= d & m . d > n . d ) } c= support m

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { d where d is Element of R : ( c <= d & m . d > n . d ) } or a in support m )
assume a in { d where d is Element of R : ( c <= d & m . d > n . d ) } ; :: thesis: a in support m
then consider d being Element of R such that
A3: ( a = d & c <= d & m . d > n . d ) ;
thus a in support m by A3, PRE_POLY:def 7; :: thesis: verum

end;

ex b being Element of R st b in { d where d is Element of R : ( c <= d & m . d > n . d ) }

proof

per cases ( m . c < n . c or m . c > n . c ) by A2, XXREAL_0:1;

suppose m . c < n . c ; :: thesis: ex b being Element of R st b in { d where d is Element of R : ( c <= d & m . d > n . d ) }

then consider d being Element of R such that
A5: ( c <= d & n . d < m . d ) by A0, HO;
take d ; :: thesis: d in { d where d is Element of R : ( c <= d & m . d > n . d ) }
thus d in { d where d is Element of R : ( c <= d & m . d > n . d ) } by A5; :: thesis: verum

end;

suppose m . c > n . c ; :: thesis: ex b being Element of R st b in { d where d is Element of R : ( c <= d & m . d > n . d ) }

then consider d being Element of R such that
A5: ( c <= d & n . d > m . d ) by A0, HO;
consider e being Element of R such that
A6: ( d <= e & n . e < m . e ) by A0, HO, A5;
take e ; :: thesis: e in { d where d is Element of R : ( c <= d & m . d > n . d ) }
c <= e by A5, A6, ORDERS_2:3;
hence e in { d where d is Element of R : ( c <= d & m . d > n . d ) } by A6; :: thesis: verum

end;

end;

end;

then consider d being Element of R such that
A7: d is_maximal_in { d where d is Element of R : ( c <= d & m . d > n . d ) } by BC, Th12;
( d in { d where d is Element of R : ( c <= d & m . d > n . d ) } & ( for a being Element of R holds
( not a in { d where d is Element of R : ( c <= d & m . d > n . d ) } or not d < a ) ) ) by A7, WAYBEL_4:55;
then consider e being Element of R such that
A8: ( d = e & c <= e & n . e < m . e ) ;
consider f being Element of R such that
A9: ( e <= f & n . f > m . f ) by A0, HO, A8;
consider g being Element of R such that
A10: ( f <= g & n . g < m . g ) by A0, HO, A9;
c <= f by A8, A9, ORDERS_2:3;
then ( c <= g & d <= g ) by A8, A9, A10, ORDERS_2:3;
then ( g in { d where d is Element of R : ( c <= d & m . d > n . d ) } & d < g ) by A10, Lem2;
hence contradiction by A7, WAYBEL_4:55; :: thesis: verum

end;

thus DershowitzMannaOrder R is transitive :: thesis: verum

proof

let a, b, c be object ; :: according to RELAT_2:def 8,ORDERS_2:def 3 :: thesis: ( not a in the carrier of (DershowitzMannaOrder R) or not b in the carrier of (DershowitzMannaOrder R) or not c in the carrier of (DershowitzMannaOrder R) or not [a,b] in the InternalRel of (DershowitzMannaOrder R) or not [b,c] in the InternalRel of (DershowitzMannaOrder R) or [a,c] in the InternalRel of (DershowitzMannaOrder R) )
assume ( a in the carrier of (DershowitzMannaOrder R) & b in the carrier of (DershowitzMannaOrder R) & c in the carrier of (DershowitzMannaOrder R) ) ; :: thesis: ( not [a,b] in the InternalRel of (DershowitzMannaOrder R) or not [b,c] in the InternalRel of (DershowitzMannaOrder R) or [a,c] in the InternalRel of (DershowitzMannaOrder R) )
then reconsider m = a, n = b, k = c as Element of (DershowitzMannaOrder R) ;
assume ( [a,b] in the InternalRel of (DershowitzMannaOrder R) & [b,c] in the InternalRel of (DershowitzMannaOrder R) ) ; :: thesis: [a,c] in the InternalRel of (DershowitzMannaOrder R)
then A0: ( m <= n & n <= k ) by ORDERS_2:def 5;
consider x1, y1 being Element of (DershowitzMannaOrder R) such that
A2: ( 1. (DershowitzMannaOrder R) <> x1 & x1 divides n & m = (n -' x1) + y1 & ( for b being Element of R st y1 . b > 0 holds
ex a being Element of R st
( x1 . a > 0 & b <= a ) ) ) by A0, DM;
consider x2, y2 being Element of (DershowitzMannaOrder R) such that
A3: ( 1. (DershowitzMannaOrder R) <> x2 & x2 divides k & n = (k -' x2) + y2 & ( for b being Element of R st y2 . b > 0 holds
ex a being Element of R st
( x2 . a > 0 & b <= a ) ) ) by A0, DM;
reconsider x = x2 + (x1 -' y2), y = (y2 -' x1) + y1 as multiset of the carrier of R by Th1;
reconsider x = x, y = y as Element of (DershowitzMannaOrder R) by Th2;
A4: ( m = (((k -' x2) + y2) -' x1) + y1 & (((k -' x2) + y2) -' x1) + y1 = (k -' x) + y ) by A2, A3, Th15;
A5: 1. (DershowitzMannaOrder R) <> x

proof

consider a being object such that
A7: ( a in the carrier of R & (1. (DershowitzMannaOrder R)) . a <> x2 . a ) by A3, PBOOLE:def 10;
reconsider a = a as Element of R by A7;
( 1. (DershowitzMannaOrder R) = 1. (finite-MultiSet_over the carrier of R) & 1. (finite-MultiSet_over the carrier of R) = EmptyBag the carrier of R ) by Th3, Th11;
then A8: (1. (DershowitzMannaOrder R)) . a = 0 by FUNCOP_1:7;
take a ; :: according to PBOOLE:def 21 :: thesis: not (1. (DershowitzMannaOrder R)) . a = x . a
( 0 < x2 . a & x2 . a <= (x2 . a) + ((x1 -' y2) . a) ) by A7, A8, NAT_1:11;
hence not (1. (DershowitzMannaOrder R)) . a = x . a by A8, PRE_POLY:def 5; :: thesis: verum

end;

A6: x divides k by A2, A3, Th15;
for b being Element of R st y . b > 0 holds
ex a being Element of R st
( x . a > 0 & b <= a )

proof

let b be Element of R; :: thesis: ( y . b > 0 implies ex a being Element of R st
( x . a > 0 & b <= a ) )
assume y . b > 0 ; :: thesis: ex a being Element of R st
( x . a > 0 & b <= a )
then ((y2 -' x1) . b) + (y1 . b) > 0 by PRE_POLY:def 5;

per cases then ( (y2 -' x1) . b > 0 or y1 . b > 0 ) ;

suppose (y2 -' x1) . b > 0 ; :: thesis: ex a being Element of R st
( x . a > 0 & b <= a )

then (y2 . b) -' (x1 . b) > 0 by PRE_POLY:def 6;
then (y2 . b) - (x1 . b) > 0 by XREAL_0:def 2;
then ( y2 . b > x1 . b & x1 . b >= 0 ) by XREAL_1:47;
then consider a being Element of R such that
B4: ( x2 . a > 0 & b <= a ) by A3;
take a ; :: thesis: ( x . a > 0 & b <= a )
( x . a = (x2 . a) + ((x1 -' y2) . a) & (x2 . a) + ((x1 -' y2) . a) >= x2 . a ) by NAT_1:11, PRE_POLY:def 5;
hence ( x . a > 0 & b <= a ) by B4; :: thesis: verum

end;

suppose y1 . b > 0 ; :: thesis: ex a being Element of R st
( x . a > 0 & b <= a )

then consider a being Element of R such that
B1: ( x1 . a > 0 & b <= a ) by A2;

per cases ( (x1 -' y2) . a > 0 or (x1 -' y2) . a = 0 ) ;

suppose B2: (x1 -' y2) . a > 0 ; :: thesis: ex a being Element of R st
( x . a > 0 & b <= a )

take a ; :: thesis: ( x . a > 0 & b <= a )
(x2 + (x1 -' y2)) . a = (x2 . a) + ((x1 -' y2) . a) by PRE_POLY:def 5;
hence x . a > 0 by B2; :: thesis: b <= a
thus b <= a by B1; :: thesis: verum

end;

suppose (x1 -' y2) . a = 0 ; :: thesis: ex a being Element of R st
( x . a > 0 & b <= a )

then (x1 . a) -' (y2 . a) = 0 by PRE_POLY:def 6;
then x1 . a <= y2 . a by NAT_D:36;
then consider c being Element of R such that
B3: ( x2 . c > 0 & a <= c ) by A3, B1;
take c ; :: thesis: ( x . c > 0 & b <= c )
x . c = (x2 . c) + ((x1 -' y2) . c) by PRE_POLY:def 5;
hence ( x . c > 0 & b <= c ) by B1, B3, ORDERS_2:3; :: thesis: verum

end;

end;

end;

end;

end;

then m <= k by A4, A5, A6, DM;
hence [a,c] in the InternalRel of (DershowitzMannaOrder R) by ORDERS_2:def 5; :: thesis: verum

end;