let OAS be OAffinSpace; 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; 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; ( 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
; a,b // f . a,f . b
A4:
a,f . a // b,f . b
by A1, A2, A3, Lm6, DIRAF:28;
now ( 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
;
a,b // f . a,f . bhence
a,
b // f . a,
f . b
by A5, A6, DIRAF:3;
verum end;
hence
a,b // f . a,f . b
by A1, A2, A3, Lm6, DIRAF:28; verum