let n be Element of NAT ; 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); 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 ; ( 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)
; ( r1 = r2 or p1 = p2 )
A2: (1 * p1) + ((- (r1 * p1)) + (r1 * p2)) =
((1 * p1) + (- (r1 * p1))) + (r1 * p2)
by EUCLID:26
.=
((1 * p1) - (r1 * p1)) + (r1 * p2)
by EUCLID:41
.=
((1 - r2) * p1) + (r2 * p2)
by A1, EUCLID:50
.=
((1 * p1) - (r2 * p1)) + (r2 * p2)
by EUCLID:50
.=
((1 * p1) + (- (r2 * p1))) + (r2 * p2)
by EUCLID:41
.=
(1 * p1) + ((- (r2 * p1)) + (r2 * p2))
by EUCLID:26
;
A3: ((r2 - r1) * p1) + (r1 * p2) =
((r2 * p1) - (r1 * p1)) + (r1 * p2)
by EUCLID:50
.=
((r2 * p1) + (- (r1 * p1))) + (r1 * p2)
by EUCLID:41
.=
(r2 * p1) + ((- (r1 * p1)) + (r1 * p2))
by EUCLID:26
.=
(r2 * p1) + ((- (r2 * p1)) + (r2 * p2))
by A2, GOBOARD7:4
.=
((r2 * p1) + (- (r2 * p1))) + (r2 * p2)
by EUCLID:26
.=
(0. (TOP-REAL n)) + (r2 * p2)
by EUCLID:36
.=
r2 * p2
by EUCLID:27
;
(r2 - r1) * p1 =
((r2 - r1) * p1) + (0. (TOP-REAL n))
by EUCLID:27
.=
((r2 - r1) * p1) + ((r1 * p2) - (r1 * p2))
by EUCLID:42
.=
(r2 * p2) - (r1 * p2)
by A3, EUCLID:45
.=
(r2 - r1) * p2
by EUCLID:50
;
then
( r2 - r1 = 0 or p1 = p2 )
by EUCLID:34;
hence
( r1 = r2 or p1 = p2 )
; verum