for a, b being Real
for Iab being non empty closed_interval Subset of REAL st a <= b & Iab = [.a,b.] holds
for Dab being Division of Iab st len Dab = 1 holds
Dab = <*b*>