let n be Element of NAT ; :: thesis: for p, q being Point of (TOP-REAL n)
for r being Real st 0 < r & p = ((1 - r) * p) + (r * q) holds
p = q
let p, q be Point of (TOP-REAL n); :: thesis: for r being Real st 0 < r & p = ((1 - r) * p) + (r * q) holds
p = q
let r be Real; :: thesis: ( 0 < r & p = ((1 - r) * p) + (r * q) implies p = q )
assume that
A1: 0 < r and
A2: p = ((1 - r) * p) + (r * q) ; :: thesis: p = q
A3: ((1 - r) * p) + (r * p) = ((1 - r) + r) * p by EUCLID:37
.= p by EUCLID:33 ;
r * p = (r * p) + (0. (TOP-REAL n)) by EUCLID:31
.= (r * p) + (((1 - r) * p) + (- ((1 - r) * p))) by EUCLID:40
.= ((r * q) + ((1 - r) * p)) + (- ((1 - r) * p)) by A2, A3, EUCLID:30
.= (r * q) + (((1 - r) * p) + (- ((1 - r) * p))) by EUCLID:30
.= (r * q) + (0. (TOP-REAL n)) by EUCLID:40
.= r * q by EUCLID:31 ;
hence p = q by A1, EUCLID:38; :: thesis: verum