let a, b, c be Real; :: thesis: for Iac, Icb being non empty compact Subset of REAL st a <= c & c <= b & Iac = [.a,c.] & Icb = [.c,b.] holds
for Dac being Division of Iac
for Dcb being Division of Icb
for i, j being Nat st i in dom Dac & j in dom Dcb & c < Dcb . 1 holds
Dac . i < Dcb . j
let Iac, Icb be non empty compact Subset of REAL; :: thesis: ( a <= c & c <= b & Iac = [.a,c.] & Icb = [.c,b.] implies for Dac being Division of Iac
for Dcb being Division of Icb
for i, j being Nat st i in dom Dac & j in dom Dcb & c < Dcb . 1 holds
Dac . i < Dcb . j )
assume that
A1: ( a <= c & c <= b ) and
A2: Iac = [.a,c.] and
A3: Icb = [.c,b.] ; :: thesis: for Dac being Division of Iac
for Dcb being Division of Icb
for i, j being Nat st i in dom Dac & j in dom Dcb & c < Dcb . 1 holds
Dac . i < Dcb . j
let Dac be Division of Iac; :: thesis: for Dcb being Division of Icb
for i, j being Nat st i in dom Dac & j in dom Dcb & c < Dcb . 1 holds
Dac . i < Dcb . j
let Dcb be Division of Icb; :: thesis: for i, j being Nat st i in dom Dac & j in dom Dcb & c < Dcb . 1 holds
Dac . i < Dcb . j
let i, j be Nat; :: thesis: ( i in dom Dac & j in dom Dcb & c < Dcb . 1 implies Dac . i < Dcb . j )
assume that
A4: i in dom Dac and
A5: j in dom Dcb ; :: thesis: ( not c < Dcb . 1 or Dac . i < Dcb . j )
assume A6: c < Dcb . 1 ; :: thesis: Dac . i < Dcb . j
i <= len Dac by A4, FINSEQ_3:25;
then ( i < len Dac or i = len Dac ) by XXREAL_0:1;
hence Dac . i < Dcb . j by A6, A1, A2, A3, A4, A5, Th43; :: thesis: verum