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:34;
now assume A5:
b <> f . a
;
:: thesis: a,b // f . a,f . b
Mid b,
f . a,
a
by A2, DIRAF:13;
then
b,
f . a // f . a,
a
by DIRAF:def 3;
then
b,
f . a // b,
a
by ANALOAF:def 5;
then A6:
a,
b // f . a,
b
by DIRAF:5;
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
f . a,
b // f . a,
f . b
by ANALOAF:def 5;
hence
a,
b // f . a,
f . b
by A5, A6, DIRAF:6;
:: thesis: verum end;
hence
a,b // f . a,f . b
by A1, A2, A3, Lm6, DIRAF:34; :: thesis: verum