let V be RealLinearSpace; 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; ( P <> R & P <> S implies cross-ratio (P,P,R,S) = 1 )
assume that
A1:
P <> R
and
A2:
P <> S
; 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
; verum