let R be non empty transitive asymmetric RelStr ; :: thesis: for a, b, c, d being Element of (DershowitzMannaOrder R)
for e being bag of the carrier of R st a <= b & e divides a & e divides b & c = a -' e & d = b -' e holds
c <= d
let a, b, c, d be Element of (DershowitzMannaOrder R); :: thesis: for e being bag of the carrier of R st a <= b & e divides a & e divides b & c = a -' e & d = b -' e holds
c <= d
let e be bag of the carrier of R; :: thesis: ( a <= b & e divides a & e divides b & c = a -' e & d = b -' e implies c <= d )
assume Z1: a <= b ; :: thesis: ( not e divides a or not e divides b or not c = a -' e or not d = b -' e or c <= d )
assume Z2: e divides a ; :: thesis: ( not e divides b or not c = a -' e or not d = b -' e or c <= d )
assume Z3: e divides b ; :: thesis: ( not c = a -' e or not d = b -' e or c <= d )
assume Z4: c = a -' e ; :: thesis: ( not d = b -' e or c <= d )
assume d = b -' e ; :: thesis: c <= d
then A0: ( a = c + e & b = d + e & a <> b ) by Z1, Z2, Z3, Z4, PRE_POLY:47;
for x being Element of R st c . x > d . x holds
ex y being Element of R st
( x <= y & c . y < d . y )
proof
let x be Element of R; :: thesis: ( c . x > d . x implies ex y being Element of R st
( x <= y & c . y < d . y ) )
assume c . x > d . x ; :: thesis: ex y being Element of R st
( x <= y & c . y < d . y )
then ( a . x = (c . x) + (e . x) & (c . x) + (e . x) > (d . x) + (e . x) & (d . x) + (e . x) = b . x ) by A0, PRE_POLY:def 5, XREAL_1:6;
then consider y being Element of R such that
A2: ( x <= y & a . y < b . y ) by Z1, HO;
take y ; :: thesis: ( x <= y & c . y < d . y )
( a . y = (c . y) + (e . y) & b . y = (d . y) + (e . y) ) by A0, PRE_POLY:def 5;
hence ( x <= y & c . y < d . y ) by A2, XREAL_1:6; :: thesis: verum
end;
hence c <= d by A0, HO; :: thesis: verum