let n be Element of NAT ; :: thesis: for p1, p2 being Point of (TOP-REAL n)
for r1, r2 being real number holds
( not ((1 - r1) * p1) + (r1 * p2) = ((1 - r2) * p1) + (r2 * p2) or r1 = r2 or p1 = p2 )
let p1, p2 be Point of (TOP-REAL n); :: thesis: for r1, r2 being real number holds
( not ((1 - r1) * p1) + (r1 * p2) = ((1 - r2) * p1) + (r2 * p2) or r1 = r2 or p1 = p2 )
let r1, r2 be real number ; :: thesis: ( not ((1 - r1) * p1) + (r1 * p2) = ((1 - r2) * p1) + (r2 * p2) or r1 = r2 or p1 = p2 )
assume A1: ((1 - r1) * p1) + (r1 * p2) = ((1 - r2) * p1) + (r2 * p2) ; :: thesis: ( r1 = r2 or p1 = p2 )
A2: (1 * p1) + ((- (r1 * p1)) + (r1 * p2)) = ((1 * p1) + (- (r1 * p1))) + (r1 * p2) by EUCLID:30
.= ((1 * p1) - (r1 * p1)) + (r1 * p2) by EUCLID:45
.= ((1 - r2) * p1) + (r2 * p2) by A1, EUCLID:54
.= ((1 * p1) - (r2 * p1)) + (r2 * p2) by EUCLID:54
.= ((1 * p1) + (- (r2 * p1))) + (r2 * p2) by EUCLID:45
.= (1 * p1) + ((- (r2 * p1)) + (r2 * p2)) by EUCLID:30 ;
A3: ((r2 - r1) * p1) + (r1 * p2) = ((r2 * p1) - (r1 * p1)) + (r1 * p2) by EUCLID:54
.= ((r2 * p1) + (- (r1 * p1))) + (r1 * p2) by EUCLID:45
.= (r2 * p1) + ((- (r1 * p1)) + (r1 * p2)) by EUCLID:30
.= (r2 * p1) + ((- (r2 * p1)) + (r2 * p2)) by A2, GOBOARD7:4
.= ((r2 * p1) + (- (r2 * p1))) + (r2 * p2) by EUCLID:30
.= (0. (TOP-REAL n)) + (r2 * p2) by EUCLID:40
.= r2 * p2 by EUCLID:31 ;
(r2 - r1) * p1 = ((r2 - r1) * p1) + (0. (TOP-REAL n)) by EUCLID:31
.= ((r2 - r1) * p1) + ((r1 * p2) - (r1 * p2)) by EUCLID:46
.= (r2 * p2) - (r1 * p2) by A3, EUCLID:49
.= (r2 - r1) * p2 by EUCLID:54 ;
then ( r2 - r1 = 0 or p1 = p2 ) by EUCLID:38;
hence ( r1 = r2 or p1 = p2 ) ; :: thesis: verum