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 & Mid a,f . a,b & a <> f . a 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 & Mid a,f . a,b & a <> f . a holds
a,b // f . a,f . b
let f be Permutation of the carrier of OAS; :: thesis: ( f is translation & Mid a,f . a,b & a <> f . a implies a,b // f . a,f . b )
assume that
A1: f is translation and
A2: Mid a,f . a,b and
A3: a <> f . a ; :: thesis: a,b // f . a,f . b
A4: a,f . a // b,f . b by A1, A2, A3, Lm6, DIRAF:28;

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

Mid b,f . a,a by A2, DIRAF:9;
then b,f . a // f . a,a by DIRAF:def 3;
then b,f . a // b,a by ANALOAF:def 5;
then A5: a,b // f . a,b by DIRAF:2;
a,f . a // f . a,b by A2, DIRAF:def 3;
then f . a,b // b,f . b by A3, A4, ANALOAF:def 5;
then A6: f . a,b // f . a,f . b by ANALOAF:def 5;
assume b <> f . a ; :: thesis: a,b // f . a,f . b
hence a,b // f . a,f . b by A5, A6, DIRAF:3; :: thesis: verum

end;

hence a,b // f . a,f . b by A1, A2, A3, Lm6, DIRAF:28; :: thesis: verum