for a, b, c being Real
for Iab, Iac, Icb being non empty compact Subset of REAL st a <= c & c <= b & Iab = [.a,b.] & Iac = [.a,c.] & Icb = [.c,b.] holds
for Dac being Division of Iac
for Dcb being Division of Icb st c < Dcb . 1 holds
Dac ^ Dcb is Division of Iab