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 ;
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 ;
then f . a,a // f . a,f . b by ANALOAF:def 5;
hence a,b // f . a,f . b by ; :: 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 ; :: 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 ; :: 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 ;
hence a,b // f . a,f . b by ; :: 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 ; :: thesis: verum
end;
hence a,b // f . a,f . b by DIRAF:4; :: thesis: verum