let OAS be OAffinSpace; for a, b being Element of OAS
for f being Permutation of the carrier of OAS st f is translation & not a,f . a,b are_collinear holds
( a,b // f . a,f . b & a,f . a // b,f . b )
let a, b be Element of OAS; for f being Permutation of the carrier of OAS st f is translation & not a,f . a,b are_collinear holds
( a,b // f . a,f . b & a,f . a // b,f . b )
let f be Permutation of the carrier of OAS; ( f is translation & not a,f . a,b are_collinear implies ( a,b // f . a,f . b & a,f . a // b,f . b ) )
assume that
A1:
f is translation
and
A2:
not a,f . a,b are_collinear
; ( a,b // f . a,f . b & a,f . a // b,f . b )
f is dilatation
by A1;
then A3:
a,b '||' f . a,f . b
by Th34;
a,f . a '||' b,f . b
by A1, Th53;
hence
( a,b // f . a,f . b & a,f . a // b,f . b )
by A2, A3, PASCH:14; verum