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) = 1 iff B = C )
let A, B, C be Element of V; :: thesis: ( A <> C & A,B,C are_collinear implies ( affine-ratio (A,B,C) = 1 iff B = C ) )
assume that
A1: A <> C and
A2: A,B,C are_collinear ; :: thesis: ( affine-ratio (A,B,C) = 1 iff B = C )
hereby :: thesis: ( B = C implies affine-ratio (A,B,C) = 1 )
assume affine-ratio (A,B,C) = 1 ; :: thesis: B = C
then B - A = 1 * (C - A) by A1, A2, Def02
.= C - A by RLVECT_1:def 8 ;
hence B = C by RLVECT_1:8; :: thesis: verum
end;
assume B = C ; :: thesis: affine-ratio (A,B,C) = 1
then B - A = 1 * (C - A) by RLVECT_1:def 8;
hence affine-ratio (A,B,C) = 1 by A1, A2, Def02; :: thesis: verum