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 ;
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 end;
then A13: p,f . p // b,f . b by ;
not p,f . p,a are_collinear
proof end;
then p,f . p // a,f . a by ;
hence a,f . a // b,f . b by ; :: thesis: verum