reconsider x = 0 , y = 1 as Point of I[01] by BORSUK_1:43;
thus 2RP . 0 = 2RP . x
.= 0 by Def6 ; :: thesis: 2RP . 1 = 1
thus 2RP . 1 = (2 * y) - 1 by Def6
.= 1 ; :: thesis: verum