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 )