for a, b, c being Real
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 holds
( ( i < len Dac implies Dac . i < Dcb . j ) & ( i = len Dac & c < Dcb . 1 implies Dac . i < Dcb . j ) & ( Dcb . 1 = c implies Dac . (len Dac) = Dcb . 1 ) )