let V be RealLinearSpace; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( affine-ratio (A,B,C) = 0 iff A = B )
hereby :: thesis: ( A = B implies affine-ratio (A,B,C) = 0 )
assume affine-ratio (A,B,C) = 0 ; :: thesis: A = B
then B - A = 0 * (C - A) by A1, A2, Def02
.= 0. V by RLVECT_1:10 ;
hence A = B by RLVECT_1:21; :: thesis: verum
end;
assume A = B ; :: thesis: 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; :: thesis: verum