let R be non empty transitive asymmetric RelStr ; :: thesis: for a, b being bag of the carrier of R
for p being partition of b -' a
for q being partition of b st q = <*a*> ^ p & q is ordered holds
p is ordered
let a, b be bag of the carrier of R; :: thesis: for p being partition of b -' a
for q being partition of b st q = <*a*> ^ p & q is ordered holds
p is ordered
let p be partition of b -' a; :: thesis: for q being partition of b st q = <*a*> ^ p & q is ordered holds
p is ordered
let q be partition of b; :: thesis: ( q = <*a*> ^ p & q is ordered implies p is ordered )
assume Z1: q = <*a*> ^ p ; :: thesis: ( not q is ordered or p is ordered )
assume Z2: q is ordered ; :: thesis: p is ordered

hereby :: according to BAGORD_2:def 10 :: thesis: ( ( for m being bag of the carrier of R st m in rng p holds
for x, y being Element of R st m . x > 0 & m . y > 0 & x <> y holds
x ## y ) & ( for m being bag of the carrier of R st m in rng p holds
m <> EmptyBag the carrier of R ) & ( for i being Nat st i in dom p & i + 1 in dom p holds
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 ) ) )

let m be bag of the carrier of R; :: thesis: ( m in rng p implies for x being Element of R st m . x > 0 holds
m . x = (b -' a) . x )
assume A0: m in rng p ; :: thesis: for x being Element of R st m . x > 0 holds
m . x = (b -' a) . x
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: ( m . x > 0 implies m . x = (b -' a) . x )
assume A2: m . x > 0 ; :: thesis: m . x = (b -' a) . x
( 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: verum

end;

hereby :: thesis: ( ( for m being bag of the carrier of R st m in rng p holds
m <> EmptyBag the carrier of R ) & ( for i being Nat st i in dom p & i + 1 in dom p holds
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 ) ) )

let m be bag of the carrier of R; :: thesis: ( m in rng p implies for x, y being Element of R st m . x > 0 & m . y > 0 & x <> y holds
x ## y )
assume m in rng p ; :: thesis: for x, y being Element of R st m . x > 0 & m . y > 0 & x <> y holds
x ## y
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: verum

end;

hereby :: thesis: for i being Nat st i in dom p & i + 1 in dom p holds
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 )

let m be bag of the carrier of R; :: thesis: ( m in rng p implies m <> EmptyBag the carrier of R )
assume m in rng p ; :: thesis: m <> EmptyBag the carrier of R
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: verum

end;

let i be Nat; :: thesis: ( i in dom p & i + 1 in dom p implies 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 ) )
assume A1: ( i in dom p & i + 1 in dom p ) ; :: thesis: 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 )
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: verum