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