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 & Mid q,p,f . q ) and
A4: LIN p,x,y ; :: thesis: x,y // f . y,f . x
A5: Mid y,p,f . y by A1, A2, A3, Th75;

A6: now

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:5; :: thesis: verum

end;

A8: now

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 LIN p,x,u by A9, 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 A15: LIN x,y,u ; :: thesis: contradiction
( LIN x,y,p & LIN x,y,x ) by A4, DIRAF:36, DIRAF:37;
hence contradiction by A10, A11, A15, DIRAF:38; :: thesis: verum

end;

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

proof

A18: 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;

LIN x,y,p by A4, 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;
A20: LIN u,r,u by DIRAF:37;
assume LIN p,u,r ; :: thesis: contradiction
then A21: LIN u,r,p by DIRAF:36;
p,x '||' p,y by A4, DIRAF:def 5;
then u,r '||' p,y by A9, A19, DIRAF:28;
then A22: LIN u,r,y by A18, A21, DIRAF:39;
LIN u,r,x by A18, A21, A19, DIRAF:39;
hence contradiction by A14, A18, A22, A20, DIRAF:38; :: thesis: verum

end;

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

end;

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