let OAS be OAffinSpace; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( 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; :: thesis: verum