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 & c < Dcb . 1 holds
Dac . i < Dcb . j