A1: 0 in { r where r is Real : ( 0 <= r & r <= 1 ) } ;
1 in { s where s is Real : ( 0 <= s & s <= 1 ) } ;
hence ( 0 in [.0,1.] & 1 in [.0,1.] ) by A1, RCOMP_1:def 1; :: thesis: verum