let R1, R2 be non empty transitive asymmetric RelStr ; :: thesis:
assume Z0: ( the carrier of R1 = the carrier of R2 & the InternalRel of R1 c= the InternalRel of R2 ) ; :: thesis:
let a, b be Element of (DershowitzMannaOrder R1); :: according to RELSET_1:def 1 :: thesis:
assume [a,b] in the InternalRel of (DershowitzMannaOrder R1) ; :: thesis:
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;

let x be Element of R2; :: thesis:
reconsider x1 = x as Element of R1 by Z0;
assume a1 . x > b1 . x ; :: thesis:
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:
[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:

end;