let R be non empty transitive asymmetric RelStr ; :: thesis: for a, b being Element of (DershowitzMannaOrder R) st a <= b holds
b <> EmptyBag the carrier of R
set DM = DershowitzMannaOrder R;
set I = the carrier of R;
set E = EmptyBag the carrier of R;
let a, b be Element of (DershowitzMannaOrder R); :: thesis: ( a <= b implies b <> EmptyBag the carrier of R )
assume Z0: a <= b ; :: thesis: b <> EmptyBag the carrier of R
per cases ( a = EmptyBag the carrier of R or a <> EmptyBag the carrier of R ) ;
suppose a = EmptyBag the carrier of R ; :: thesis: b <> EmptyBag the carrier of R
hence b <> EmptyBag the carrier of R by Z0; :: thesis: verum
end;
suppose A1: a <> EmptyBag the carrier of R ; :: thesis: b <> EmptyBag the carrier of R
EmptyBag the carrier of R divides a by PRE_POLY:59;
then ( [(EmptyBag the carrier of R),a] in DivOrder the carrier of R & DivOrder the carrier of R c= the InternalRel of (DershowitzMannaOrder R) ) by A1, DO, Th16;
hence b <> EmptyBag the carrier of R by Z0, ORDERS_2:def 5; :: thesis: verum
end;
end;