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 & a <> f . a & LIN a,f . a,b holds
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 & a <> f . a & LIN a,f . a,b holds
a,f . a // b,f . b
let f be Permutation of the carrier of OAS; :: thesis: ( f is translation & a <> f . a & LIN a,f . a,b implies a,f . a // b,f . b )
assume that
A1: f is translation and
A2: a <> f . a and
A3: LIN a,f . a,b ; :: thesis: a,f . a // b,f . b
consider p being Element of OAS such that
A4: not LIN a,f . a,p by A2, DIRAF:37;
A5: f is dilatation by A1, Def9;
A6: f <> id the carrier of OAS by A2, FUNCT_1:18;
then A7: p <> f . p by A1, Def9;
A8: b <> f . b by A1, A6, Def9;
not LIN p,f . p,b

proof

A9: LIN p,f . p,p by DIRAF:31;
assume A10: LIN p,f . p,b ; :: thesis: contradiction
then LIN p,f . p,f . b by A5, Th60;
then A11: LIN b,f . b,p by A7, A10, A9, DIRAF:32;
( LIN a,f . a,f . b & LIN a,f . a,a ) by A3, A5, Th60, DIRAF:31;
then A12: LIN b,f . b,a by A2, A3, DIRAF:32;
then LIN b,f . b,f . a by A5, Th60;
hence contradiction by A4, A8, A12, A11, DIRAF:32; :: thesis: verum

end;

then A13: p,f . p // b,f . b by A1, Lm5;
not LIN p,f . p,a

proof

assume A14: LIN p,f . p,a ; :: thesis: contradiction
then ( LIN p,f . p,p & LIN p,f . p,f . a ) by A5, Th60, DIRAF:31;
hence contradiction by A4, A7, A14, DIRAF:32; :: thesis: verum

end;

then p,f . p // a,f . a by A1, Lm5;
hence a,f . a // b,f . b by A7, A13, ANALOAF:def 5; :: thesis: verum