let AFS be AffinSpace; for x, y being Element of AFS
for f being Permutation of the carrier of AFS st f is dilatation & LIN x,f . x,y holds
LIN x,f . x,f . y
let x, y be Element of AFS; for f being Permutation of the carrier of AFS st f is dilatation & LIN x,f . x,y holds
LIN x,f . x,f . y
let f be Permutation of the carrier of AFS; ( f is dilatation & LIN x,f . x,y implies LIN x,f . x,f . y )
assume A1:
f is dilatation
; ( not LIN x,f . x,y or LIN x,f . x,f . y )
assume A2:
LIN x,f . x,y
; LIN x,f . x,f . y
now ( x <> y implies LIN x,f . x,f . y )assume A3:
x <> y
;
LIN x,f . x,f . y
(
x,
f . x // x,
y &
x,
y // f . x,
f . y )
by A1, A2, Th68, AFF_1:def 1;
then
x,
f . x // f . x,
f . y
by A3, AFF_1:5;
then
f . x,
x // f . x,
f . y
by AFF_1:4;
then
LIN f . x,
x,
f . y
by AFF_1:def 1;
hence
LIN x,
f . x,
f . y
by AFF_1:6;
verum end;
hence
LIN x,f . x,f . y
by AFF_1:7; verum