let OAS be OAffinSpace; :: thesis: for p, q, x, y being Element of OAS
for f being Permutation of the carrier of OAS st f is dilatation & f . p = p & q <> p & Mid q,p,f . q & p,x,y are_collinear holds
x,y // f . y,f . x

let p, q, x, y be Element of OAS; :: thesis: for f being Permutation of the carrier of OAS st f is dilatation & f . p = p & q <> p & Mid q,p,f . q & p,x,y are_collinear holds
x,y // f . y,f . x

let f be Permutation of the carrier of OAS; :: thesis: ( f is dilatation & f . p = p & q <> p & Mid q,p,f . q & p,x,y are_collinear implies x,y // f . y,f . x )
assume that
A1: f is dilatation and
A2: f . p = p and
A3: ( q <> p & Mid q,p,f . q ) and
A4: p,x,y are_collinear ; :: thesis: x,y // f . y,f . x
A5: Mid y,p,f . y by A1, A2, A3, Th60;
A6: now :: thesis: ( x = p implies x,y // f . y,f . x )
assume A7: x = p ; :: thesis: x,y // f . y,f . x
then y,x // x,f . y by ;
hence x,y // f . y,f . x by ; :: thesis: verum
end;
A8: now :: thesis: ( x <> p & y <> p & x <> y implies x,y // f . y,f . x )
assume that
A9: x <> p and
y <> p and
A10: x <> y ; :: thesis: x,y // f . y,f . x
consider u being Element of OAS such that
A11: not p,x,u are_collinear by ;
consider r being Element of OAS such that
A12: x,y '||' u,r and
A13: x,u '||' y,r by DIRAF:26;
A14: not x,y,u are_collinear
proof end;
then A16: x,y // u,r by ;
A17: not p,u,r are_collinear
proof end;
then A23: u <> r by DIRAF:31;
set u9 = f . u;
set r9 = f . r;
set x9 = f . x;
set y9 = f . y;
A24: not f . x,f . y,f . u are_collinear by ;
( f . x,f . y '||' f . u,f . r & f . x,f . u '||' f . y,f . r ) by A1, A12, A13, Th45;
then f . x,f . y // f . u,f . r by ;
then A25: f . r,f . u // f . y,f . x by DIRAF:2;
u,r // f . r,f . u by A1, A2, A3, A17, Th61;
then x,y // f . r,f . u by ;
hence x,y // f . y,f . x by ; :: thesis: verum
end;
Mid x,p,f . x by A1, A2, A3, Th60;
hence x,y // f . y,f . x by ; :: thesis: verum