let OAS be OAffinSpace; :: thesis: for x, y being Element of OAS
for f being Permutation of the carrier of OAS st f is dilatation & x,f . x,y are_collinear holds
x,f . x,f . y are_collinear
let x, y be Element of OAS; :: thesis: for f being Permutation of the carrier of OAS st f is dilatation & x,f . x,y are_collinear holds
x,f . x,f . y are_collinear
let f be Permutation of the carrier of OAS; :: thesis: ( f is dilatation & x,f . x,y are_collinear implies x,f . x,f . y are_collinear )
assume A1: f is dilatation ; :: thesis: ( not x,f . x,y are_collinear or x,f . x,f . y are_collinear )
assume A2: x,f . x,y are_collinear ; :: thesis: x,f . x,f . y are_collinear

now :: thesis: ( x <> y implies x,f . x,f . y are_collinear )

assume A3: x <> y ; :: thesis: x,f . x,f . y are_collinear
( x,f . x '||' x,y & x,y '||' f . x,f . y ) by A1, A2, Th34, DIRAF:def 5;
then x,f . x '||' f . x,f . y by A3, DIRAF:23;
then f . x,x '||' f . x,f . y by DIRAF:22;
then f . x,x,f . y are_collinear by DIRAF:def 5;
hence x,f . x,f . y are_collinear by DIRAF:30; :: thesis: verum

end;

hence x,f . x,f . y are_collinear by DIRAF:31; :: thesis: verum