for a, b being Real
for Iab being non empty compact Subset of REAL
for Dab being Division of Iab st 2 <= len Dab holds
Dab /^ 1 is Division of Iab