let R be non empty transitive asymmetric RelStr ; :: thesis: DivOrder the carrier of R c= the InternalRel of (DershowitzMannaOrder R)
set DM = DershowitzMannaOrder R;
let a, b be Element of Bags the carrier of R; :: according to RELSET_1:def 1 :: thesis: ( not [a,b] in DivOrder the carrier of R or [a,b] in the InternalRel of (DershowitzMannaOrder R) )
assume A1: [a,b] in DivOrder the carrier of R ; :: thesis: [a,b] in the InternalRel of (DershowitzMannaOrder R)
reconsider a = a, b = b as multiset of the carrier of R by Th1;
reconsider a = a, b = b as Element of (DershowitzMannaOrder R) by Th2;
A2: ( a <> b & a divides b ) by A1, DO;
then for x being Element of R st a . x > b . x holds
ex y being Element of R st
( x <= y & a . y < b . y ) by PRE_POLY:def 11;
then a <= b by A2, HO;
hence [a,b] in the InternalRel of (DershowitzMannaOrder R) by ORDERS_2:def 5; :: thesis: verum