let R be non empty transitive asymmetric RelStr ; :: thesis: for b being bag of the carrier of R
for x being Element of R
for q being partition of b st q is ordered & (q /. 1) . x = 0 & b . x > 0 holds
ex y being Element of R st
( (q /. 1) . y > 0 & x <= y )
let b be bag of the carrier of R; :: thesis: for x being Element of R
for q being partition of b st q is ordered & (q /. 1) . x = 0 & b . x > 0 holds
ex y being Element of R st
( (q /. 1) . y > 0 & x <= y )
let x be Element of R; :: thesis: for q being partition of b st q is ordered & (q /. 1) . x = 0 & b . x > 0 holds
ex y being Element of R st
( (q /. 1) . y > 0 & x <= y )
let q be partition of b; :: thesis: ( q is ordered & (q /. 1) . x = 0 & b . x > 0 implies ex y being Element of R st
( (q /. 1) . y > 0 & x <= y ) )
assume Z0: q is ordered ; :: thesis: ( not (q /. 1) . x = 0 or not b . x > 0 or ex y being Element of R st
( (q /. 1) . y > 0 & x <= y ) )
assume Z2: (q /. 1) . x = 0 ; :: thesis: ( not b . x > 0 or ex y being Element of R st
( (q /. 1) . y > 0 & x <= y ) )
assume Z3: b . x > 0 ; :: thesis: ex y being Element of R st
( (q /. 1) . y > 0 & x <= y )
defpred S₁[ Nat] means ( $1 in dom q implies for x being Element of R st (q /. $1) . x > 0 holds
ex y being Element of R st
( (q /. 1) . y > 0 & x <= y ) );
A1: S₁[2]

proof

assume A2: 2 in dom q ; :: thesis: for x being Element of R st (q /. 2) . x > 0 holds
ex y being Element of R st
( (q /. 1) . y > 0 & x <= y )
then 2 <= len q by FINSEQ_3:25;
then 1 <= len q by XXREAL_0:2;
then ( 1 in dom q & 2 = 1 + 1 ) by FINSEQ_3:25;
hence for x being Element of R st (q /. 2) . x > 0 holds
ex y being Element of R st
( (q /. 1) . y > 0 & x <= y ) by A2, Z0; :: thesis: verum

end;

A3: for i being Nat st 2 <= i & S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( 2 <= i & S₁[i] implies S₁[i + 1] )
assume A4: ( 2 <= i & S₁[i] & i + 1 in dom q ) ; :: thesis: for x being Element of R st (q /. (i + 1)) . x > 0 holds
ex y being Element of R st
( (q /. 1) . y > 0 & x <= y )
then ( i <= i + 1 & i + 1 <= len q ) by NAT_1:11, FINSEQ_3:25;
then A0: ( 1 <= i & i <= len q ) by A4, XXREAL_0:2;
then A5: i in dom q by FINSEQ_3:25;
let x be Element of R; :: thesis: ( (q /. (i + 1)) . x > 0 implies ex y being Element of R st
( (q /. 1) . y > 0 & x <= y ) )
assume (q /. (i + 1)) . x > 0 ; :: thesis: ex y being Element of R st
( (q /. 1) . y > 0 & x <= y )
then consider y being Element of R such that
A6: ( (q /. i) . y > 0 & x <= y ) by Z0, A4, A5;
consider z being Element of R such that
A7: ( (q /. 1) . z > 0 & y <= z ) by A4, A0, A6, FINSEQ_3:25;
take z ; :: thesis: ( (q /. 1) . z > 0 & x <= z )
thus (q /. 1) . z > 0 by A7; :: thesis: x <= z
thus x <= z by A6, A7, ORDERS_2:3; :: thesis: verum

end;

A8: for i being Nat st i >= 2 holds
S₁[i] from NAT_1:sch 8(A1, A3);
b = Sum q by PART;
then consider i being Nat such that
A9: ( i in dom q & (q /. i) . x > 0 ) by Z3, Lem14;
( 1 <= i & i <> 1 ) by A9, Z2, FINSEQ_3:25;
then 1 < i by XXREAL_0:1;
then 1 + 1 <= i by NAT_1:13;
hence ex y being Element of R st
( (q /. 1) . y > 0 & x <= y ) by A8, A9; :: thesis: verum