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 & b <> f . a & Mid a,b,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 & a <> f . a & b <> f . a & Mid a,b,f . a holds
a,b // f . a,f . b

let f be Permutation of the carrier of OAS; :: thesis: ( f is translation & a <> f . a & b <> f . a & Mid a,b,f . a implies a,b // f . a,f . b )
assume that
A1: f is translation and
A2: a <> f . a and
A3: b <> f . a and
A4: Mid a,b,f . a ; :: thesis: a,b // f . a,f . b
A5: a,b // b,f . a by ;
A6: f is dilatation by A1;
A7: a,b,f . a are_collinear by ;
then A8: a,f . a,b are_collinear by DIRAF:30;
A9: f <> id the carrier of OAS by A2;
now :: thesis: ( a <> b implies a,b // f . a,f . b )
assume A10: a <> b ; :: thesis: a,b // f . a,f . b
A11: now :: thesis: not a,b // f . b,f . a
f . a,a,b are_collinear by ;
then f . a,a '||' f . a,b by DIRAF:def 5;
then A12: a,f . a '||' b,f . a by DIRAF:22;
consider q being Element of OAS such that
A13: not a,f . a,q are_collinear by ;
consider x being Element of OAS such that
A14: q,b // b,x and
A15: q,a // f . a,x by ;
A16: a,q // x,f . a by ;
A17: Mid q,b,x by ;
then A18: x,b,q are_collinear by ;
A19: x <> f . a A22: not x,f . a,b are_collinear
proof
assume x,f . a,b are_collinear ; :: thesis: contradiction
then f . a,x,b are_collinear by DIRAF:30;
then A23: f . a,x '||' f . a,b by DIRAF:def 5;
f . a,b,a are_collinear by ;
then A24: f . a,b '||' f . a,a by DIRAF:def 5;
q,a '||' f . a,x by ;
then f . a,b '||' q,a by ;
then f . a,a '||' q,a by ;
then a,f . a '||' a,q by DIRAF:22;
hence contradiction by A13, DIRAF:def 5; :: thesis: verum
end;
a,f . a // q,f . q by A1, A13, Lm5;
then a,f . a '||' q,f . q by DIRAF:def 4;
then b,f . a '||' q,f . q by ;
then A25: f . a,b '||' q,f . q by DIRAF:22;
A26: a,f . a,f . b are_collinear by A6, A8, Th47;
( a,q // f . a,f . q & a <> q ) by ;
then f . a,f . q // x,f . a by ;
then f . a,f . q '||' f . a,x by DIRAF:def 4;
then f . a,f . q,x are_collinear by DIRAF:def 5;
then A27: x,f . a,f . q are_collinear by DIRAF:30;
A28: b <> f . b by A1, A9;
a,f . a,f . a are_collinear by DIRAF:31;
then A29: b,f . b,f . a are_collinear by ;
a,f . a,a are_collinear by DIRAF:31;
then b,f . b,a are_collinear by ;
then A30: not b,f . b,q are_collinear by ;
A31: not b,f . b,f . q are_collinear
proof
b,f . b '||' q,f . q by ;
then A32: b,f . b '||' f . q,q by DIRAF:22;
assume b,f . b,f . q are_collinear ; :: thesis: contradiction
hence contradiction by A28, A30, A32, DIRAF:33; :: thesis: verum
end;
then A33: f . b <> f . q by DIRAF:31;
( a,b // a,f . a & a,f . a // b,f . b ) by ;
then A34: a,b // b,f . b by ;
assume a,b // f . b,f . a ; :: thesis: contradiction
then b,f . b // f . b,f . a by ;
then Mid b,f . b,f . a by DIRAF:def 3;
then A35: Mid f . a,f . b,b by DIRAF:9;
A36: x,b,b are_collinear by DIRAF:31;
Mid x,b,q by ;
then Mid x,f . a,f . q by ;
then consider y being Element of OAS such that
A37: Mid x,y,b and
A38: Mid y,f . b,f . q by ;
x,y,b are_collinear by ;
then A39: x,b,y are_collinear by DIRAF:30;
A40: x <> b by ;
then b,q,y are_collinear by ;
then A41: b,q '||' b,y by DIRAF:def 5;
A42: y,f . b,f . q are_collinear by ;
then f . b,f . q,y are_collinear by DIRAF:30;
then A43: f . b,f . q '||' f . b,y by DIRAF:def 5;
b,q '||' f . b,f . q by ;
then b,q '||' f . b,y by ;
then f . b,y '||' b,y by ;
then y,b '||' y,f . b by DIRAF:22;
then A44: y,b,f . b are_collinear by DIRAF:def 5;
A45: y,b,b are_collinear by DIRAF:31;
y,b,q are_collinear by ;
hence contradiction by A42, A30, A31, A44, A45, DIRAF:32; :: thesis: verum
end;
a,b '||' f . a,f . b by ;
hence a,b // f . a,f . b by ; :: thesis: verum
end;
hence a,b // f . a,f . b by DIRAF:4; :: thesis: verum