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