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 ;
now :: thesis: ( b <> f . a implies a,b // f . a,f . b )
Mid b,f . a,a by ;
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 ;
then f . a,b // b,f . b by ;
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 ; :: thesis: verum
end;
hence a,b // f . a,f . b by ; :: thesis: verum