let OAS be OAffinSpace; 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; 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; ( f is dilatation & x,f . x,y are_collinear implies x,f . x,f . y are_collinear )
assume A1:
f is dilatation
; ( not x,f . x,y are_collinear or x,f . x,f . y are_collinear )
assume A2:
x,f . x,y are_collinear
; x,f . x,f . y are_collinear
now ( x <> y implies x,f . x,f . y are_collinear )assume A3:
x <> y
;
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;
verum end;
hence
x,f . x,f . y are_collinear
by DIRAF:31; verum