A1: ( 0 is Point of I[01] & 1 is Point of I[01] ) by BORSUK_1:86;
hence 3RP . 0 = (1 / 2) * 0 by Def9
.= 0 ;
:: thesis: 3RP . 1 = 1
thus 3RP . 1 = (2 * 1) - 1 by A1, Def9
.= 1 ; :: thesis: verum