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 EUCLID:36;
then 0. (TOP-REAL n) = p1 - (((1 / 2) * p1) + ((1 / 2) * p2)) by A2, EUCLID:46
.= (p1 - ((1 / 2) * p1)) - ((1 / 2) * p2) by EUCLID:50
.= ((1 * p1) - ((1 / 2) * p1)) - ((1 / 2) * p2) by EUCLID:33
.= ((1 - (1 / 2)) * p1) - ((1 / 2) * p2) by EUCLID:54
.= (1 / 2) * (p1 - p2) by EUCLID:53 ;
then p1 - p2 = 0. (TOP-REAL n) by EUCLID:35;
hence contradiction by A1, EUCLID:47; :: thesis: verum