let V be RealLinearSpace; :: thesis: for P, R, S being Element of V st P <> R & P <> S holds
cross-ratio (P,P,R,S) = 1
let P, R, S be Element of V; :: thesis: ( P <> R & P <> S implies cross-ratio (P,P,R,S) = 1 )
assume that
A1: P <> R and
A2: P <> S ; :: thesis: cross-ratio (P,P,R,S) = 1
( R,P,P are_collinear & S,P,P are_collinear ) by Th05;
then ( affine-ratio (R,P,P) = 1 & affine-ratio (S,P,P) = 1 ) by A1, A2, Th07;
hence cross-ratio (P,P,R,S) = 1 ; :: thesis: verum