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,b // f . a,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,b // f . a,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,b // f . a,f . b )
assume that
A1: f is translation and
A2: a <> f . a and
A3: a,f . a,b are_collinear ; :: thesis: a,b // f . a,f . b
f <> id the carrier of OAS by A2;
then A4: b <> f . b by A1;
A5: f is dilatation by A1;

now :: thesis: ( a <> b implies a,b // f . a,f . b )

assume A6: a <> b ; :: thesis: a,b // f . a,f . b

A7: now :: thesis: ( Mid f . a,a,b implies a,b // f . a,f . b )

assume A8: Mid f . a,a,b ; :: thesis: a,b // f . a,f . b

A9: now :: thesis: ( Mid f . b,b,a implies a,b // f . a,f . b )

assume Mid f . b,b,a ; :: thesis: a,b // f . a,f . b
then Mid a,b,f . b by DIRAF:9;
then a,b // b,f . b by DIRAF:def 3;
then A10: a,b // a,f . b by ANALOAF:def 5;
Mid b,a,f . a by A8, DIRAF:9;
then b,a // a,f . a by DIRAF:def 3;
then A11: a,b // f . a,a by ANALOAF:def 5;
then f . a,a // a,f . b by A6, A10, ANALOAF:def 5;
then f . a,a // f . a,f . b by ANALOAF:def 5;
hence a,b // f . a,f . b by A10, A11, DIRAF:3; :: thesis: verum

end;

A12: now :: thesis: ( Mid b,a,f . b implies a,b // f . a,f . b )

A13: now :: thesis: ( a = f . b implies a,b // f . a,f . b )

assume A14: a = f . b ; :: thesis: a,b // f . a,f . b
a,f . a // b,f . b by A1, A2, A3, Lm6;
hence a,b // f . a,f . b by A14, DIRAF:2; :: thesis: verum

end;

assume Mid b,a,f . b ; :: thesis: a,b // f . a,f . b
then ( b,a // f . b,f . a or a = f . b ) by A1, A4, Lm8;
hence a,b // f . a,f . b by A13, DIRAF:2; :: thesis: verum

end;

A15: now :: thesis: ( Mid b,f . b,a implies a,b // f . a,f . b )

assume Mid b,f . b,a ; :: thesis: a,b // f . a,f . b
then b,a // f . b,f . a by A1, A4, Lm7;
hence a,b // f . a,f . b by DIRAF:2; :: thesis: verum

end;

( a,f . a,f . b are_collinear & a,f . a,a are_collinear ) by A3, A5, Th47, DIRAF:31;
hence a,b // f . a,f . b by A2, A3, A15, A12, A9, DIRAF:29, DIRAF:32; :: thesis: verum

end;

A16: now :: thesis: ( Mid a,b,f . a implies a,b // f . a,f . b )

assume A17: Mid a,b,f . a ; :: thesis: a,b // f . a,f . b
( b = f . a implies a,b // f . a,f . b ) by A1, A2, A3, Lm6;
hence a,b // f . a,f . b by A1, A2, A17, Lm8; :: thesis: verum

end;

( Mid a,f . a,b implies a,b // f . a,f . b ) by A1, A2, Lm7;
hence a,b // f . a,f . b by A3, A7, A16, DIRAF:29; :: thesis: verum

end;

hence a,b // f . a,f . b by DIRAF:4; :: thesis: verum