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,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 & LIN a,f . a,b holds
a,b // f . a,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,b // f . a,f . b )
assume A1: ( f is translation & a <> f . a & LIN a,f . a,b ) ; :: thesis: a,b // f . a,f . b
then f <> id the carrier of OAS by FUNCT_1:35;
then A2: b <> f . b by A1, Def9;
A3: f is dilatation by A1, Def9;

now

assume A4: a <> b ; :: thesis: a,b // f . a,f . b
A5: ( Mid a,f . a,b implies a,b // f . a,f . b ) by A1, Lm7;

A6: now

assume A7: Mid f . a,a,b ; :: thesis: a,b // f . a,f . b
A8: ( LIN a,f . a,f . b & LIN a,f . a,a ) by A1, A3, Th60, DIRAF:37;

A9: now

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

end;

A10: now

assume Mid b,a,f . b ; :: thesis: a,b // f . a,f . b
then A11: ( b,a // f . b,f . a or a = f . b ) by A1, A2, Lm8;

now

assume a = f . b ; :: thesis: a,b // f . a,f . b
then ( a = f . b & a,f . a // b,f . b ) by A1, Lm6;
hence a,b // f . a,f . b by DIRAF:5; :: thesis: verum

end;

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

end;

now

assume Mid f . b,b,a ; :: thesis: a,b // f . a,f . b
then ( Mid a,b,f . b & Mid b,a,f . a ) by A7, DIRAF:13;
then ( a,b // b,f . b & b,a // a,f . a ) by DIRAF:def 3;
then A12: ( a,b // a,f . b & a,b // f . a,a ) by ANALOAF:def 5;
then f . a,a // a,f . b by A4, ANALOAF:def 5;
then f . a,a // f . a,f . b by ANALOAF:def 5;
hence a,b // f . a,f . b by A12, DIRAF:6; :: thesis: verum

end;

hence a,b // f . a,f . b by A1, A8, A9, A10, DIRAF:35, DIRAF:38; :: thesis: verum

end;

now

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

end;

hence a,b // f . a,f . b by A1, A5, A6, DIRAF:35; :: thesis: verum

end;

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