theorem :: MEASURE6:17

for A being non empty Interval st A is closed_interval holds
A = [.(inf A),(sup A).]