let R be non empty transitive asymmetric RelStr ; :: thesis: for a, b, c being bag of the carrier of R
for x being Element of R
for p being partition of b -' a
for q being partition of b st q is ordered & q = <*a*> ^ p & c in rng p & c . x > 0 holds
ex y being Element of R st
( a . y > 0 & x <= y )
let a, b, c be bag of the carrier of R; :: thesis: for x being Element of R
for p being partition of b -' a
for q being partition of b st q is ordered & q = <*a*> ^ p & c in rng p & c . x > 0 holds
ex y being Element of R st
( a . y > 0 & x <= y )
let x be Element of R; :: thesis: for p being partition of b -' a
for q being partition of b st q is ordered & q = <*a*> ^ p & c in rng p & c . x > 0 holds
ex y being Element of R st
( a . y > 0 & x <= y )
let p be partition of b -' a; :: thesis: for q being partition of b st q is ordered & q = <*a*> ^ p & c in rng p & c . x > 0 holds
ex y being Element of R st
( a . y > 0 & x <= y )
let q be partition of b; :: thesis: ( q is ordered & q = <*a*> ^ p & c in rng p & c . x > 0 implies ex y being Element of R st
( a . y > 0 & x <= y ) )
assume Z0: q is ordered ; :: thesis: ( not q = <*a*> ^ p or not c in rng p or not c . x > 0 or ex y being Element of R st
( a . y > 0 & x <= y ) )
assume Z1: q = <*a*> ^ p ; :: thesis: ( not c in rng p or not c . x > 0 or ex y being Element of R st
( a . y > 0 & x <= y ) )
assume c in rng p ; :: thesis: ( not c . x > 0 or ex y being Element of R st
( a . y > 0 & x <= y ) )
then consider i being object such that
A1: ( i in dom p & c = p . i ) by FUNCT_1:def 3;
reconsider i = i as Nat by A1;
A2: ( 1 <= i & p . i = p /. i ) by A1, FINSEQ_3:25, PARTFUN1:def 6;
defpred S₁[ Nat] means ( $1 in dom p implies for x being Element of R st (p /. $1) . x > 0 holds
ex y being Element of R st
( a . y > 0 & x <= y ) );
A5: ( len <*a*> = 1 & dom <*a*> c= dom q ) by Z1, FINSEQ_1:26, FINSEQ_1:40;
A3: S₁[1]

proof

assume A4: 1 in dom p ; :: thesis: for x being Element of R st (p /. 1) . x > 0 holds
ex y being Element of R st
( a . y > 0 & x <= y )
then A6: 1 + 1 in dom q by Z1, A5, FINSEQ_1:28;
B0: 1 in dom <*a*> by A5, FINSEQ_3:25;
then ( 1 in dom q & q . 1 = <*a*> . 1 & <*a*> . 1 = a ) by Z1, A5, FINSEQ_1:def 7;
then ( q /. 1 = a & q /. 2 = q . 2 & q . 2 = p . 1 & p . 1 = p /. 1 ) by Z1, A4, A5, A6, FINSEQ_1:def 7, PARTFUN1:def 6;
hence for x being Element of R st (p /. 1) . x > 0 holds
ex y being Element of R st
( a . y > 0 & x <= y ) by Z0, A6, A5, B0; :: thesis: verum

end;

A8: for i being Nat st i >= 1 & S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( i >= 1 & S₁[i] implies S₁[i + 1] )
assume B1: ( i >= 1 & S₁[i] & 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
( a . y > 0 & x <= y )
then ( i < i + 1 & i + 1 <= len p ) by NAT_1:13, FINSEQ_3:25;
then BB: i <= len p by XXREAL_0:2;
then B3: i in dom p by B1, FINSEQ_3:25;
B4: ( 1 + i in dom q & (1 + i) + 1 in dom q ) by Z1, A5, B1, BB, FINSEQ_3:25, FINSEQ_1:28;
B5: ( q /. (1 + i) = q . (1 + i) & q . (1 + i) = p . i & p . i = p /. i & q /. ((1 + i) + 1) = q . ((1 + i) + 1) & q . ((1 + i) + 1) = p . (i + 1) & p . (i + 1) = p /. (i + 1) ) by Z1, A5, B1, B3, FINSEQ_1:28, FINSEQ_1:def 7, PARTFUN1:def 6;
let x be Element of R; :: thesis: ( (p /. (i + 1)) . x > 0 implies ex y being Element of R st
( a . y > 0 & x <= y ) )
assume (p /. (i + 1)) . x > 0 ; :: thesis: ex y being Element of R st
( a . y > 0 & x <= y )
then consider y being Element of R such that
B6: ( (p /. i) . y > 0 & x <= y ) by Z0, B4, B5;
consider z being Element of R such that
B7: ( a . z > 0 & y <= z ) by BB, B1, FINSEQ_3:25, B6;
take z ; :: thesis: ( a . z > 0 & x <= z )
thus ( a . z > 0 & x <= z ) by B6, B7, ORDERS_2:3; :: thesis: verum

end;

for i being Nat st i >= 1 holds
S₁[i] from NAT_1:sch 8(A3, A8);
hence ( not c . x > 0 or ex y being Element of R st
( a . y > 0 & x <= y ) ) by A1, A2; :: thesis: verum