let R1, R2 be non empty transitive asymmetric RelStr ; :: thesis: ( the carrier of R1 = the carrier of R2 & the InternalRel of R1 c= the InternalRel of R2 implies the InternalRel of (DershowitzMannaOrder R1) c= the InternalRel of (DershowitzMannaOrder R2) )
assume Z0: ( the carrier of R1 = the carrier of R2 & the InternalRel of R1 c= the InternalRel of R2 ) ; :: thesis: the InternalRel of (DershowitzMannaOrder R1) c= the InternalRel of (DershowitzMannaOrder R2)
let a, b be Element of (DershowitzMannaOrder R1); :: according to RELSET_1:def 1 :: thesis: ( not [a,b] in the InternalRel of (DershowitzMannaOrder R1) or [a,b] in the InternalRel of (DershowitzMannaOrder R2) )
assume [a,b] in the InternalRel of (DershowitzMannaOrder R1) ; :: thesis: [a,b] in the InternalRel of (DershowitzMannaOrder R2)
then A3: a <= b by ORDERS_2:def 5;
then A1: ( a <> b & ( for x being Element of R1 st a . x > b . x holds
ex y being Element of R1 st
( x <= y & a . y < b . y ) ) ) by HO;
reconsider b1 = b, a1 = a as multiset of the carrier of R1 by Th1;
reconsider b1 = b1, a1 = a1 as Element of (DershowitzMannaOrder R2) by Z0, Th2;

now :: thesis: for x being Element of R2 st a1 . x > b1 . x holds
ex y1 being Element of R2 st
( x <= y1 & a1 . y1 < b1 . y1 )

let x be Element of R2; :: thesis: ( a1 . x > b1 . x implies ex y1 being Element of R2 st
( x <= y1 & a1 . y1 < b1 . y1 ) )
reconsider x1 = x as Element of R1 by Z0;
assume a1 . x > b1 . x ; :: thesis: ex y1 being Element of R2 st
( x <= y1 & a1 . y1 < b1 . y1 )
then consider y being Element of R1 such that
A2: ( x1 <= y & a . y < b . y ) by A3, HO;
reconsider y1 = y as Element of R2 by Z0;
take y1 = y1; :: thesis: ( x <= y1 & a1 . y1 < b1 . y1 )
[x1,y] in the InternalRel of R1 by A2, ORDERS_2:def 5;
hence ( x <= y1 & a1 . y1 < b1 . y1 ) by Z0, A2, ORDERS_2:def 5; :: thesis: verum

end;

then a1 <= b1 by A1, HO;
hence [a,b] in the InternalRel of (DershowitzMannaOrder R2) by ORDERS_2:def 5; :: thesis: verum