0 is Point of I[01] by BORSUK_1:43;
hence 3RP . 0 = (1 / 2) * 0 by Def7
.= 0 ;
:: thesis: 3RP . 1 = 1
1 is Point of I[01] by BORSUK_1:43;
hence 3RP . 1 = (2 * 1) - 1 by Def7
.= 1 ;
:: thesis: verum