let R be non empty transitive asymmetric RelStr ; 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; 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; 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; 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; ( 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
; ( 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
; ( 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
; ( 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 S1[ 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:
S1[1]
proof
assume A4:
1
in dom p
;
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, FINSEQ_1:40;
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;
verum
end;
A8:
for i being Nat st i >= 1 & S1[i] holds
S1[i + 1]
proof
let i be
Nat;
( i >= 1 & S1[i] implies S1[i + 1] )
assume B1:
(
i >= 1 &
S1[
i] &
i + 1
in dom p )
;
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;
( (p /. (i + 1)) . x > 0 implies ex y being Element of R st
( a . y > 0 & x <= y ) )
assume
(p /. (i + 1)) . x > 0
;
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
;
( a . z > 0 & x <= z )
thus
(
a . z > 0 &
x <= z )
by B6, B7, ORDERS_2:3;
verum
end;
for i being Nat st i >= 1 holds
S1[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; verum