let V be RealLinearSpace; for A, B, C being Element of V st A <> C & A,B,C are_collinear holds
( affine-ratio (A,B,C) = 0 iff A = B )
let A, B, C be Element of V; ( A <> C & A,B,C are_collinear implies ( affine-ratio (A,B,C) = 0 iff A = B ) )
assume that
A1:
A <> C
and
A2:
A,B,C are_collinear
; ( affine-ratio (A,B,C) = 0 iff A = B )
assume
A = B
; affine-ratio (A,B,C) = 0
then B - A =
0. V
by RLVECT_1:5
.=
0 * (C - A)
by RLVECT_1:10
;
hence
affine-ratio (A,B,C) = 0
by A1, A2, Def02; verum