let R be non empty transitive asymmetric RelStr ; :: thesis: for a being bag of the carrier of R holds
( <*a*> is ordered iff ( a <> EmptyBag the carrier of R & ( for x, y being Element of R st a . x > 0 & a . y > 0 & x <> y holds
x ## y ) ) )
let a be bag of the carrier of R; :: thesis: ( <*a*> is ordered iff ( a <> EmptyBag the carrier of R & ( for x, y being Element of R st a . x > 0 & a . y > 0 & x <> y holds
x ## y ) ) )
hereby :: thesis: ( a <> EmptyBag the carrier of R & ( for x, y being Element of R st a . x > 0 & a . y > 0 & x <> y holds
x ## y ) implies <*a*> is ordered )
assume Z0: <*a*> is ordered ; :: thesis: ( a <> EmptyBag the carrier of R & ( for x, y being Element of R st a . x > 0 & a . y > 0 & x <> y holds
x ## y ) )
( a in {a} & {a} = rng <*a*> ) by TARSKI:def 1, FINSEQ_1:39;
hence ( a <> EmptyBag the carrier of R & ( for x, y being Element of R st a . x > 0 & a . y > 0 & x <> y holds
x ## y ) ) by Z0; :: thesis: verum
end;
assume Z3: a <> EmptyBag the carrier of R ; :: thesis: ( ex x, y being Element of R st
( a . x > 0 & a . y > 0 & x <> y & not x ## y ) or <*a*> is ordered )
assume Z4: for x, y being Element of R st a . x > 0 & a . y > 0 & x <> y holds
x ## y ; :: thesis: <*a*> is ordered
set p = <*a*>;
hereby :: according to BAGORD_2:def 10 :: thesis: ( ( for m being bag of the carrier of R st m in rng <*a*> 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 <*a*> holds
m <> EmptyBag the carrier of R ) & ( for i being Nat st i in dom <*a*> & i + 1 in dom <*a*> holds
for x being Element of R st (<*a*> /. (i + 1)) . x > 0 holds
ex y being Element of R st
( (<*a*> /. i) . y > 0 & x <= y ) ) )
let m be bag of the carrier of R; :: thesis: ( m in rng <*a*> implies for x being Element of R st m . x > 0 holds
m . x = a . x )
assume m in rng <*a*> ; :: thesis: for x being Element of R st m . x > 0 holds
m . x = a . x
then m in {a} by FINSEQ_1:39;
hence for x being Element of R st m . x > 0 holds
m . x = a . x by TARSKI:def 1; :: thesis: verum
end;
hereby :: thesis: ( ( for m being bag of the carrier of R st m in rng <*a*> holds
m <> EmptyBag the carrier of R ) & ( for i being Nat st i in dom <*a*> & i + 1 in dom <*a*> holds
for x being Element of R st (<*a*> /. (i + 1)) . x > 0 holds
ex y being Element of R st
( (<*a*> /. i) . y > 0 & x <= y ) ) )
let m be bag of the carrier of R; :: thesis: ( m in rng <*a*> implies for x, y being Element of R st m . x > 0 & m . y > 0 & x <> y holds
x ## y )
assume m in rng <*a*> ; :: thesis: for x, y being Element of R st m . x > 0 & m . y > 0 & x <> y holds
x ## y
then m in {a} by FINSEQ_1:39;
then m = a by TARSKI:def 1;
hence for x, y being Element of R st m . x > 0 & m . y > 0 & x <> y holds
x ## y by Z4; :: thesis: verum
end;
hereby :: thesis: for i being Nat st i in dom <*a*> & i + 1 in dom <*a*> holds
for x being Element of R st (<*a*> /. (i + 1)) . x > 0 holds
ex y being Element of R st
( (<*a*> /. i) . y > 0 & x <= y )
let m be bag of the carrier of R; :: thesis: ( m in rng <*a*> implies m <> EmptyBag the carrier of R )
assume m in rng <*a*> ; :: thesis: m <> EmptyBag the carrier of R
then m in {a} by FINSEQ_1:39;
hence m <> EmptyBag the carrier of R by Z3, TARSKI:def 1; :: thesis: verum
end;
let i be Nat; :: thesis: ( i in dom <*a*> & i + 1 in dom <*a*> implies for x being Element of R st (<*a*> /. (i + 1)) . x > 0 holds
ex y being Element of R st
( (<*a*> /. i) . y > 0 & x <= y ) )
assume ( i in dom <*a*> & i + 1 in dom <*a*> ) ; :: thesis: for x being Element of R st (<*a*> /. (i + 1)) . x > 0 holds
ex y being Element of R st
( (<*a*> /. i) . y > 0 & x <= y )
then ( 1 <= i & i < i + 1 & i + 1 <= len <*a*> & len <*a*> = 1 ) by FINSEQ_1:40, FINSEQ_3:25, NAT_1:13;
hence for x being Element of R st (<*a*> /. (i + 1)) . x > 0 holds
ex y being Element of R st
( (<*a*> /. i) . y > 0 & x <= y ) by XXREAL_0:2; :: thesis: verum