for A being non empty closed_interval Subset of REAL
for D1, D2 being Division of A ex D being Division of A st
( D1 <= D & D2 <= D & rng D = (rng D1) \/ (rng D2) )