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

proof

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

end;

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

proof

assume A14: p,f . p,a are_collinear ; :: thesis: contradiction
then ( p,f . p,p are_collinear & p,f . p,f . a are_collinear ) by A5, Th47, 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