theorem :: BORSUK_1:43

for r being Real holds
( ( 0 <= r & r <= 1 ) iff r in the carrier of I[01] )