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 A5, DIRAF:def 3;
hence x,y // f . y,f . x by A2, A7, DIRAF:2; :: 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 A9, DIRAF:37;
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

assume A15: x,y,u are_collinear ; :: thesis: contradiction
( x,y,p are_collinear & x,y,x are_collinear ) by A4, DIRAF:30, DIRAF:31;
hence contradiction by A10, A11, A15, DIRAF:32; :: thesis: verum

end;

then A16: x,y // u,r by A12, A13, PASCH:14;
A17: not p,u,r are_collinear

proof

A18: now :: thesis: not u = r

assume u = r ; :: thesis: contradiction
then u,x '||' u,y by A13, DIRAF:22;
then u,x,y are_collinear by DIRAF:def 5;
hence contradiction by A14, DIRAF:30; :: thesis: verum

end;

x,y,p are_collinear by A4, DIRAF:30;
then x,y '||' x,p by DIRAF:def 5;
then x,y '||' p,x by DIRAF:22;
then A19: u,r '||' p,x by A10, A12, DIRAF:23;
A20: u,r,u are_collinear by DIRAF:31;
assume p,u,r are_collinear ; :: thesis: contradiction
then A21: u,r,p are_collinear by DIRAF:30;
p,x '||' p,y by A4, DIRAF:def 5;
then u,r '||' p,y by A9, A19, DIRAF:23;
then A22: u,r,y are_collinear by A18, A21, DIRAF:33;
u,r,x are_collinear by A18, A21, A19, DIRAF:33;
hence contradiction by A14, A18, A22, A20, DIRAF:32; :: thesis: verum

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 A1, A14, Th46;
( 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 A24, PASCH:14;
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 A16, A23, DIRAF:3;
hence x,y // f . y,f . x by A25, A23, DIRAF:3, FUNCT_2:58; :: thesis: verum

end;

Mid x,p,f . x by A1, A2, A3, Th60;
hence x,y // f . y,f . x by A2, A6, A8, DIRAF:4, DIRAF:def 3; :: thesis: verum