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 & LIN p,x,y 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 & LIN p,x,y 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 & LIN p,x,y implies x,y // f . y,f . x )
assume that
A1: f is dilatation and
A2: f . p = p and
A3: q <> p and
A4: Mid q,p,f . q and
A5: LIN p,x,y ; :: thesis: x,y // f . y,f . x
A6: Mid x,p,f . x by A1, A2, A3, A4, Th75;
A7: Mid y,p,f . y by A1, A2, A3, A4, Th75;

A8: now

assume A9: x = p ; :: thesis: x,y // f . y,f . x
then y,x // x,f . y by A7, DIRAF:def 3;
hence x,y // f . y,f . x by A2, A9, DIRAF:5; :: thesis: verum

end;

now

assume A10: ( x <> p & y <> p & x <> y ) ; :: thesis: x,y // f . y,f . x
then consider u being Element of OAS such that
A11: not LIN p,x,u by DIRAF:43;
consider r being Element of OAS such that
A12: x,y '||' u,r and
A13: x,u '||' y,r by DIRAF:31;
A14: not LIN x,y,u

proof

assume LIN x,y,u ; :: thesis: contradiction
then ( LIN x,y,u & LIN x,y,p & LIN x,y,x ) by A5, DIRAF:36, DIRAF:37;
hence contradiction by A10, A11, DIRAF:38; :: thesis: verum

end;

then A15: x,y // u,r by A12, A13, PASCH:21;
A16: not LIN p,u,r

proof

A17: now

assume u = r ; :: thesis: contradiction
then u,x '||' u,y by A13, DIRAF:27;
then LIN u,x,y by DIRAF:def 5;
hence contradiction by A14, DIRAF:36; :: thesis: verum

end;

assume LIN p,u,r ; :: thesis: contradiction
then A18: LIN u,r,p by DIRAF:36;
LIN x,y,p by A5, DIRAF:36;
then x,y '||' x,p by DIRAF:def 5;
then x,y '||' p,x by DIRAF:27;
then A19: u,r '||' p,x by A10, A12, DIRAF:28;
then A20: LIN u,r,x by A17, A18, DIRAF:39;
p,x '||' p,y by A5, DIRAF:def 5;
then u,r '||' p,y by A10, A19, DIRAF:28;
then ( LIN u,r,y & LIN u,r,u ) by A17, A18, DIRAF:37, DIRAF:39;
hence contradiction by A14, A17, A20, DIRAF:38; :: thesis: verum

end;

then A21: u,r // f . r,f . u by A1, A2, A3, A4, Th76;
set u' = f . u;
set r' = f . r;
set x' = f . x;
set y' = f . y;
( f . x,f . y '||' f . u,f . r & f . x,f . u '||' f . y,f . r & not LIN f . x,f . y,f . u ) by A1, A12, A13, A14, Th58, Th59;
then f . x,f . y // f . u,f . r by PASCH:21;
then A22: f . r,f . u // f . y,f . x by DIRAF:5;
A23: u <> r by A16, DIRAF:37;
then x,y // f . r,f . u by A15, A21, DIRAF:6;
hence x,y // f . y,f . x by A22, A23, DIRAF:6, FUNCT_2:85; :: thesis: verum

end;

hence x,y // f . y,f . x by A2, A6, A8, DIRAF:7, DIRAF:def 3; :: thesis: verum