let r be Real; :: thesis: for p, q, s being Point of (TOP-REAL 2) st s = ((1 - r) * p) + (r * q) & s <> p & 0 <= r holds
0 < r
let p, q, s be Point of (TOP-REAL 2); :: thesis: ( s = ((1 - r) * p) + (r * q) & s <> p & 0 <= r implies 0 < r )
assume that
A1: s = ((1 - r) * p) + (r * q) and
A2: s <> p and
A3: 0 <= r ; :: thesis: 0 < r
assume A4: r <= 0 ; :: thesis: contradiction
then s = ((1 - 0) * p) + (r * q) by A1, A3
.= ((1 - 0) * p) + (0 * q) by A3, A4
.= (1 * p) + (0. (TOP-REAL 2)) by RLVECT_1:10
.= 1 * p by RLVECT_1:4
.= p by RLVECT_1:def 8 ;
hence contradiction by A2; :: thesis: verum