let R be non empty transitive asymmetric RelStr ; :: thesis:
let a, b be bag of the carrier of R; :: thesis:
let p be partition of b -' a; :: thesis:
let q be partition of b; :: thesis:
assume Z1: q = <*a*> ^ p ; :: thesis:
assume Z2: q is ordered ; :: thesis:

hereby :: according to BAGORD_2:def 10 :: thesis:

let m be bag of the carrier of R; :: thesis:
assume A0: m in rng p ; :: thesis:
then A1: ( m in (rng <*a*>) \/ (rng p) & (rng <*a*>) \/ (rng p) = rng q ) by Z1, XBOOLE_0:def 3, FINSEQ_1:31;
let x be Element of R; :: thesis:
assume A2: m . x > 0 ; :: thesis:
( m divides Sum p & Sum p = b -' a & b -' a divides b ) by A0, Th26, PART, Lem3;
then ( b . x = m . x & m . x <= (b -' a) . x & (b -' a) . x <= b . x ) by A1, A2, Z2, PRE_POLY:def 11;
hence m . x = (b -' a) . x by XXREAL_0:1; :: thesis:

end;

hereby :: thesis:

let m be bag of the carrier of R; :: thesis:
assume m in rng p ; :: thesis:
then ( m in (rng <*a*>) \/ (rng p) & (rng <*a*>) \/ (rng p) = rng q ) by Z1, FINSEQ_1:31, XBOOLE_0:def 3;
hence for x, y being Element of R st m . x > 0 & m . y > 0 & x <> y holds
x ## y by Z2; :: thesis:

end;

hereby :: thesis:

let m be bag of the carrier of R; :: thesis:
assume m in rng p ; :: thesis:
then ( m in (rng <*a*>) \/ (rng p) & (rng <*a*>) \/ (rng p) = rng q ) by Z1, FINSEQ_1:31, XBOOLE_0:def 3;
hence m <> EmptyBag the carrier of R by Z2; :: thesis:

end;

let i be Nat; :: thesis:
assume A1: ( i in dom p & i + 1 in dom p ) ; :: thesis:
A2: len <*a*> = 1 by FINSEQ_1:40;
then A3: ( q . (1 + i) = p . i & q . (1 + (i + 1)) = p . (i + 1) ) by Z1, A1, FINSEQ_1:def 7;
A4: ( 1 + i in dom q & (1 + i) + 1 = 1 + (i + 1) & 1 + (i + 1) in dom q ) by Z1, A1, A2, FINSEQ_1:28;
then ( q . (1 + i) = q /. (1 + i) & p /. i = p . i & q . (1 + (i + 1)) = q /. ((1 + i) + 1) & p . (i + 1) = p /. (i + 1) ) by A1, PARTFUN1:def 6;
hence for x being Element of R st (p /. (i + 1)) . x > 0 holds
ex y being Element of R st
( (p /. i) . y > 0 & x <= y ) by Z2, A3, A4; :: thesis: