let M be strict RelExtension of finite-MultiSet_over the carrier of R; :: thesis:

assume A1: M = DershowitzMannaOrder R ; :: thesis:
let m, n be Element of M; :: thesis:

assume m <= n ; :: thesis:
then consider x, y being Element of M such that
A2: ( 1. M <> x & x divides n & m = (n -' x) + y & ( for b being Element of R st y . b > 0 holds
ex a being Element of R st
( x . a > 0 & b <= a ) ) ) by A1, DM;
set X = { a where a is Element of R : ( x . a > 0 & ex b being Element of R st
( y . b > 0 & b <= a ) ) } ;
B1: { a where a is Element of R : ( x . a > 0 & ex b being Element of R st
( y . b > 0 & b <= a ) ) } c= support x

proof

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume a in { a where a is Element of R : ( x . a > 0 & ex b being Element of R st
( y . b > 0 & b <= a ) ) } ; :: thesis:
then consider c being Element of R such that
A3: ( a = c & x . c > 0 & ex b being Element of R st
( y . b > 0 & b <= c ) ) ;
thus a in support x by A3, PRE_POLY:def 7; :: thesis:

end;

x <> y

proof

per cases by Th3;

suppose y = 1. M ; :: thesis:

hence x <> y by A2; :: thesis:

end;

suppose y <> 1. (finite-MultiSet_over the carrier of R) ; :: thesis:

then y <> EmptyBag the carrier of R by Th11;
then consider b being object such that
A5: ( b in the carrier of R & y . b <> ( the carrier of R --> 0) . b ) by PBOOLE:def 10;
reconsider b = b as Element of R by A5;
A6: ( 0 <= y . b & y . b <> 0 ) by A5, FUNCOP_1:7;
then consider a being Element of R such that
A7: ( x . a > 0 & b <= a ) by A2;
a in { a where a is Element of R : ( x . a > 0 & ex b being Element of R st
( y . b > 0 & b <= a ) ) } by A6, A7;
then consider c being Element of R such that
A8: c is_maximal_in { a where a is Element of R : ( x . a > 0 & ex b being Element of R st
( y . b > 0 & b <= a ) ) } by B1, Th12;
A9: ( c in { a where a is Element of R : ( x . a > 0 & ex b being Element of R st
( y . b > 0 & b <= a ) ) } & ( for a being Element of R holds
( not a in { a where a is Element of R : ( x . a > 0 & ex b being Element of R st
( y . b > 0 & b <= a ) ) } or not c < a ) ) ) by A8, WAYBEL_4:55;
not c in support y

proof

assume c in support y ; :: thesis:
then A11: ( 0 <= y . c & y . c <> 0 ) by PRE_POLY:def 7;
then consider a being Element of R such that
A12: ( x . a > 0 & c <= a ) by A2;
( a in { a where a is Element of R : ( x . a > 0 & ex b being Element of R st
( y . b > 0 & b <= a ) ) } & c < a ) by A11, A12, Lem2;
hence contradiction by A8, WAYBEL_4:55; :: thesis:

end;

hence x <> y by B1, A9; :: thesis:

end;

hence m <> n by A2, Th9; :: thesis:
let a be Element of R; :: thesis:
assume m . a > n . a ; :: thesis:
then (m . a) - (n . a) > 0 by XREAL_1:50;
then (m . a) -' (n . a) > 0 by XREAL_0:def 2;
then A3: (m -' n) . a > 0 by PRE_POLY:def 6;
m -' n divides y by A2, Th8;
then y . a > 0 by A3, PRE_POLY:def 11;
then consider b being Element of R such that
A4: ( x . b > 0 & a <= b ) by A2;
set X = { c where c is Element of R : ( x . c > 0 & a <= c ) } ;
{ c where c is Element of R : ( x . c > 0 & a <= c ) } c= support x

proof

let b be object ; :: according to TARSKI:def 3 :: thesis:
assume b in { c where c is Element of R : ( x . c > 0 & a <= c ) } ; :: thesis:
then consider c being Element of R such that
B2: ( b = c & x . c > 0 & a <= c ) ;
thus b in support x by B2, PRE_POLY:def 7; :: thesis:

end;

then ( { c where c is Element of R : ( x . c > 0 & a <= c ) } is finite & b in { c where c is Element of R : ( x . c > 0 & a <= c ) } ) by A4;
then consider c being Element of R such that
B3: c is_maximal_in { c where c is Element of R : ( x . c > 0 & a <= c ) } by Th12;
( c in { c where c is Element of R : ( x . c > 0 & a <= c ) } & ( for a being Element of R holds
( not a in { c where c is Element of R : ( x . c > 0 & a <= c ) } or not c < a ) ) ) by B3, WAYBEL_4:55;
then consider d being Element of R such that
B5: ( c = d & x . d > 0 & a <= d ) ;
take c = c; :: thesis:
thus a <= c by B5; :: thesis:
assume m . c >= n . c ; :: thesis:

per cases by XXREAL_0:1;

suppose m . c > n . c ; :: thesis:

then (m . c) - (n . c) > 0 by XREAL_1:50;
then ( (m . c) -' (n . c) > 0 & m -' n divides y ) by A2, Th8, XREAL_0:def 2;
then ( y . c >= (m -' n) . c & (m -' n) . c > 0 ) by PRE_POLY:def 6, PRE_POLY:def 11;
then consider e being Element of R such that
B6: ( x . e > 0 & c <= e ) by A2;
a <= e by B5, B6, YELLOW_0:def 2;
then ( e in { c where c is Element of R : ( x . c > 0 & a <= c ) } & c < e ) by B6, Lem2;
hence contradiction by B3, WAYBEL_4:55; :: thesis:

end;

suppose m . c = n . c ; :: thesis:

then ( x . c = (x . c) -' 0 & (x . c) -' 0 = (x . c) -' ((n . c) -' (m . c)) & (x . c) -' ((n . c) -' (m . c)) = (x . c) -' ((n -' m) . c) & (x . c) -' ((n -' m) . c) = (x -' (n -' m)) . c & (x -' (n -' m)) . c = (y -' (m -' n)) . c & (y -' (m -' n)) . c = (y . c) -' ((m -' n) . c) & (y . c) -' ((m -' n) . c) = (y . c) -' ((m . c) -' (n . c)) & (y . c) -' ((m . c) -' (n . c)) = (y . c) -' 0 & (y . c) -' 0 = y . c ) by A2, Th8A, XREAL_1:232, NAT_D:40, PRE_POLY:def 6;
then consider e being Element of R such that
B6: ( x . e > 0 & c <= e ) by A2, B5;
a <= e by B5, B6, YELLOW_0:def 2;
then ( e in { c where c is Element of R : ( x . c > 0 & a <= c ) } & c < e ) by B6, Lem2;
hence contradiction by B3, WAYBEL_4:55; :: thesis:

end;

assume A5: ( 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 ) ) ) ; :: thesis:
reconsider x = n -' m, y = m -' n as multiset of the carrier of R by Th1;
reconsider x = x, y = y as Element of M by Th2;
A6: m = (n -' x) + y by Th7;
A8: x divides n by Lem3;

A9: now :: thesis:

let b be Element of R; :: thesis:
assume y . b > 0 ; :: thesis:
then (m . b) -' (n . b) > 0 by PRE_POLY:def 6;
then (m . b) - (n . b) > 0 by XREAL_0:def 2;
then consider a being Element of R such that
A7: ( b <= a & m . a < n . a ) by A5, XREAL_1:47;
take a = a; :: thesis:
(n . a) - (m . a) > 0 by A7, XREAL_1:50;
then (n . a) -' (m . a) > 0 by XREAL_0:def 2;
hence ( x . a > 0 & b <= a ) by A7, PRE_POLY:def 6; :: thesis:

end;

1. M <> x

proof

per cases by A5, Lem4;

suppose EmptyBag the carrier of R <> x ; :: thesis:

then 1. (finite-MultiSet_over the carrier of R) <> x by Th11;
hence 1. M <> x by Th3; :: thesis:

end;

suppose EmptyBag the carrier of R <> y ; :: thesis:

then consider b being object such that
A10: ( b in the carrier of R & (EmptyBag the carrier of R) . b <> y . b ) by PBOOLE:def 10;
reconsider b = b as Element of R by A10;
( 0 <> y . b & y . b >= 0 ) by A10, FUNCOP_1:7;
then consider a being Element of R such that
A11: ( x . a > 0 & b <= a ) by A9;
take a ; :: according to PBOOLE:def 21 :: thesis:
( EmptyBag the carrier of R = 1. (finite-MultiSet_over the carrier of R) & 1. (finite-MultiSet_over the carrier of R) = 1. M ) by Th11, Th3;
hence not (1. M) . a = x . a by A11, FUNCOP_1:7; :: thesis:

end;

hence m <= n by A1, A6, A8, A9, DM; :: thesis:

end;

assume B1: for m, n being Element of M holds
( m <= n iff ( 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 ) ) ) ) ; :: thesis:
for m, n being Element of M holds
( m <= n iff ex x, y being Element of M st
( 1. M <> x & x divides n & m = (n -' x) + y & ( 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 m, n be Element of M; :: thesis:

hereby :: thesis:

assume Z0: m <= n ; :: thesis:
reconsider x = n -' m, y = m -' n as multiset of the carrier of R by Th1;
reconsider x = x, y = y as Element of M by Th2;
take x = x; :: thesis:
take y = y; :: thesis:

A9: now :: thesis:

let b be Element of R; :: thesis:
assume y . b > 0 ; :: thesis:
then (m . b) -' (n . b) > 0 by PRE_POLY:def 6;
then (m . b) - (n . b) > 0 by XREAL_0:def 2;
then consider a being Element of R such that
A7: ( b <= a & m . a < n . a ) by Z0, B1, XREAL_1:47;
take a = a; :: thesis:
(n . a) - (m . a) > 0 by A7, XREAL_1:50;
then (n . a) -' (m . a) > 0 by XREAL_0:def 2;
hence ( x . a > 0 & b <= a ) by A7, PRE_POLY:def 6; :: thesis:

end;

thus 1. M <> x :: thesis:

proof

per cases by Z0, B1, Lem4;

suppose EmptyBag the carrier of R <> x ; :: thesis:

then 1. (finite-MultiSet_over the carrier of R) <> x by Th11;
hence 1. M <> x by Th3; :: thesis:

end;

suppose EmptyBag the carrier of R <> y ; :: thesis:

end;

thus x divides n by Lem3; :: thesis:
thus m = (n -' x) + y by Th7; :: thesis:
let b be Element of R; :: thesis:
assume y . b > 0 ; :: thesis:
hence ex a being Element of R st
( x . a > 0 & b <= a ) by A9; :: thesis:

end;

given x, y being Element of M such that A2: ( 1. M <> x & x divides n & m = (n -' x) + y & ( for b being Element of R st y . b > 0 holds
ex a being Element of R st
( x . a > 0 & b <= a ) ) ) ; :: thesis:

now :: thesis:

set X = { a where a is Element of R : ( x . a > 0 & ex b being Element of R st
( y . b > 0 & b <= a ) ) } ;
B1: { a where a is Element of R : ( x . a > 0 & ex b being Element of R st
( y . b > 0 & b <= a ) ) } c= support x

proof