let AFS be AffinSpace; :: thesis: for x, y, z being Element of AFS

for f being Permutation of the carrier of AFS st f is collineation holds

( LIN x,y,z iff LIN f . x,f . y,f . z )

let x, y, z be Element of AFS; :: thesis: for f being Permutation of the carrier of AFS st f is collineation holds

( LIN x,y,z iff LIN f . x,f . y,f . z )

let f be Permutation of the carrier of AFS; :: thesis: ( f is collineation implies ( LIN x,y,z iff LIN f . x,f . y,f . z ) )

assume f is collineation ; :: thesis: ( LIN x,y,z iff LIN f . x,f . y,f . z )

then ( x,y // x,z iff f . x,f . y // f . x,f . z ) by Th87;

hence ( LIN x,y,z iff LIN f . x,f . y,f . z ) by AFF_1:def 1; :: thesis: verum

for f being Permutation of the carrier of AFS st f is collineation holds

( LIN x,y,z iff LIN f . x,f . y,f . z )

let x, y, z be Element of AFS; :: thesis: for f being Permutation of the carrier of AFS st f is collineation holds

( LIN x,y,z iff LIN f . x,f . y,f . z )

let f be Permutation of the carrier of AFS; :: thesis: ( f is collineation implies ( LIN x,y,z iff LIN f . x,f . y,f . z ) )

assume f is collineation ; :: thesis: ( LIN x,y,z iff LIN f . x,f . y,f . z )

then ( x,y // x,z iff f . x,f . y // f . x,f . z ) by Th87;

hence ( LIN x,y,z iff LIN f . x,f . y,f . z ) by AFF_1:def 1; :: thesis: verum