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