let n be Element of NAT ; :: thesis: for p1, p2 being Point of (TOP-REAL n) st p1 <> p2 holds
(1 / 2) * (p1 + p2) <> p1
let p1, p2 be Point of (TOP-REAL n); :: thesis: ( p1 <> p2 implies (1 / 2) * (p1 + p2) <> p1 )
set r = 1 / 2;
assume that
A1: p1 <> p2 and
A2: (1 / 2) * (p1 + p2) = p1 ; :: thesis: contradiction
(1 / 2) * (p1 + p2) = ((1 / 2) * p1) + ((1 / 2) * p2) by RLVECT_1:def 5;
then 0. (TOP-REAL n) = p1 - (((1 / 2) * p1) + ((1 / 2) * p2)) by A2, RLVECT_1:5
.= (p1 - ((1 / 2) * p1)) - ((1 / 2) * p2) by RLVECT_1:27
.= ((1 * p1) - ((1 / 2) * p1)) - ((1 / 2) * p2) by RLVECT_1:def 8
.= ((1 - (1 / 2)) * p1) - ((1 / 2) * p2) by RLVECT_1:35
.= (1 / 2) * (p1 - p2) by RLVECT_1:34 ;
then p1 - p2 = 0. (TOP-REAL n) by RLVECT_1:11;
hence contradiction by A1, RLVECT_1:21; :: thesis: verum