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 LIN a,f . a,b 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 LIN a,f . a,b 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 LIN a,f . a,b implies ( a,b // f . a,f . b & a,f . a // b,f . b ) )
assume that
A1: f is translation and
A2: not LIN a,f . a,b ; :: thesis: ( a,b // f . a,f . b & a,f . a // b,f . b )
A3: f is dilatation by A1, Def9;
then A4: a,b '||' f . a,f . b by Th51;
a,f . a '||' b,f . b by A1, A3, Th67;
hence ( a,b // f . a,f . b & a,f . a // b,f . b ) by A2, A4, PASCH:14; :: thesis: verum