let r be Real; :: thesis: ( ( 0 <= r & r <= 1 ) iff r in the carrier of I[01] )
A1: [.0,1.] = { r1 where r1 is Real : ( 0 <= r1 & r1 <= 1 ) } by RCOMP_1:def 1;
thus ( 0 <= r & r <= 1 implies r in the carrier of I[01] ) by A1, BORSUK_1:40; :: thesis: ( r in the carrier of I[01] implies ( 0 <= r & r <= 1 ) )
assume r in the carrier of I[01] ; :: thesis: ( 0 <= r & r <= 1 )
then ex r2 being Real st
( r2 = r & 0 <= r2 & r2 <= 1 ) by A1, BORSUK_1:40;
hence ( 0 <= r & r <= 1 ) ; :: thesis: verum