let r be real number ; :: thesis: ( ( 0 <= r & r <= 1 ) iff r in the carrier of I[01] )
A1: r is Real by XREAL_0:def 1;
A2: [.0 ,1.] = { r1 where r1 is Real : ( 0 <= r1 & r1 <= 1 ) } by RCOMP_1:def 1;
hence ( 0 <= r & r <= 1 implies r in the carrier of I[01] ) by A1, BORSUK_1:83; :: 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 consider r2 being Real such that
A3: ( r2 = r & 0 <= r2 & r2 <= 1 ) by A2, BORSUK_1:83;
thus ( 0 <= r & r <= 1 ) by A3; :: thesis: verum