let R be non empty transitive asymmetric RelStr ; :: thesis: ( the InternalRel of R is empty implies the InternalRel of (DershowitzMannaOrder R) = DivOrder the carrier of R )
assume Z0: the InternalRel of R is empty ; :: thesis: the InternalRel of (DershowitzMannaOrder R) = DivOrder the carrier of R
let a be object ; :: according to RELAT_1:def 2 :: thesis: for b₁ being object holds
( ( not [a,b₁] in the InternalRel of (DershowitzMannaOrder R) or [a,b₁] in DivOrder the carrier of R ) & ( not [a,b₁] in DivOrder the carrier of R or [a,b₁] in the InternalRel of (DershowitzMannaOrder R) ) )
let b be object ; :: thesis: ( ( not [a,b] in the InternalRel of (DershowitzMannaOrder R) or [a,b] in DivOrder the carrier of R ) & ( not [a,b] in DivOrder the carrier of R or [a,b] in the InternalRel of (DershowitzMannaOrder R) ) )

hereby :: thesis: ( not [a,b] in DivOrder the carrier of R or [a,b] in the InternalRel of (DershowitzMannaOrder R) )

assume A1: [a,b] in the InternalRel of (DershowitzMannaOrder R) ; :: thesis: [a,b] in DivOrder the carrier of R
then reconsider m = a, n = b as Element of (DershowitzMannaOrder R) by ZFMISC_1:87;
A5: m <= n by A1, ORDERS_2:def 5;
then A3: ( 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 ) ) ) by HO;
m divides n

proof

let a be object ; :: according to PRE_POLY:def 11 :: thesis: m . a <= n . a
assume A4: m . a > n . a ; :: thesis: contradiction
a in dom m by A4, FUNCT_1:def 2;
then reconsider a = a as Element of R ;
consider b being Element of R such that
A2: ( a <= b & m . b < n . b ) by A5, HO, A4;
thus contradiction by Z0, A2, ORDERS_2:def 5; :: thesis: verum

end;

hence [a,b] in DivOrder the carrier of R by A3, DO; :: thesis: verum

end;

DivOrder the carrier of R c= the InternalRel of (DershowitzMannaOrder R) by Th16;
hence ( not [a,b] in DivOrder the carrier of R or [a,b] in the InternalRel of (DershowitzMannaOrder R) ) ; :: thesis: verum