let R be non empty transitive asymmetric RelStr ; :: thesis: for a, b being bag of the carrier of R
for y being Element of R
for q being partition of b
for c being bag of the carrier of R
for r being Bags the carrier of R -valued FinSequence st q is ordered & q = <*a,c*> ^ r & c . y > 0 holds
ex x being Element of R st
( a . x > 0 & y <= x )
let a, b be bag of the carrier of R; :: thesis: for y being Element of R
for q being partition of b
for c being bag of the carrier of R
for r being Bags the carrier of R -valued FinSequence st q is ordered & q = <*a,c*> ^ r & c . y > 0 holds
ex x being Element of R st
( a . x > 0 & y <= x )
let y be Element of R; :: thesis: for q being partition of b
for c being bag of the carrier of R
for r being Bags the carrier of R -valued FinSequence st q is ordered & q = <*a,c*> ^ r & c . y > 0 holds
ex x being Element of R st
( a . x > 0 & y <= x )
let q be partition of b; :: thesis: for c being bag of the carrier of R
for r being Bags the carrier of R -valued FinSequence st q is ordered & q = <*a,c*> ^ r & c . y > 0 holds
ex x being Element of R st
( a . x > 0 & y <= x )
let c be bag of the carrier of R; :: thesis: for r being Bags the carrier of R -valued FinSequence st q is ordered & q = <*a,c*> ^ r & c . y > 0 holds
ex x being Element of R st
( a . x > 0 & y <= x )
let r be Bags the carrier of R -valued FinSequence; :: thesis: ( q is ordered & q = <*a,c*> ^ r & c . y > 0 implies ex x being Element of R st
( a . x > 0 & y <= x ) )
assume Z0: q is ordered ; :: thesis: ( not q = <*a,c*> ^ r or not c . y > 0 or ex x being Element of R st
( a . x > 0 & y <= x ) )
assume Z1: q = <*a,c*> ^ r ; :: thesis: ( not c . y > 0 or ex x being Element of R st
( a . x > 0 & y <= x ) )
assume Z2: c . y > 0 ; :: thesis: ex x being Element of R st
( a . x > 0 & y <= x )
len <*a,c*> = 2 by FINSEQ_1:44;
then A1: ( 1 in dom <*a,c*> & 2 in dom <*a,c*> & dom <*a,c*> c= dom q ) by Z1, FINSEQ_1:26, FINSEQ_3:25;
( q /. 1 = q . 1 & q . 1 = <*a,c*> . 1 & <*a,c*> . 1 = a & q /. (1 + 1) = q . 2 & q . 2 = <*a,c*> . 2 & <*a,c*> . 2 = c ) by Z1, A1, PARTFUN1:def 6, FINSEQ_1:def 7, FINSEQ_1:44;
hence ex x being Element of R st
( a . x > 0 & y <= x ) by Z0, Z2, A1; :: thesis: verum