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, Th40; :: 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, Th40;

hence ( 0 <= r & r <= 1 ) ; :: thesis: verum

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, Th40; :: 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, Th40;

hence ( 0 <= r & r <= 1 ) ; :: thesis: verum