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