let OAS be OAffinSpace; :: thesis: for p, q, x being Element of OAS
for f being Permutation of the carrier of OAS st f is dilatation & f . p = p & Mid q,p,f . q & q <> p holds
Mid x,p,f . x
let p, q, x be Element of OAS; :: thesis: for f being Permutation of the carrier of OAS st f is dilatation & f . p = p & Mid q,p,f . q & q <> p holds
Mid x,p,f . x
let f be Permutation of the carrier of OAS; :: thesis: ( f is dilatation & f . p = p & Mid q,p,f . q & q <> p implies Mid x,p,f . x )
assume that
A1: ( f is dilatation & f . p = p ) and
A2: Mid q,p,f . q and
A3: q <> p ; :: thesis: Mid x,p,f . x

now :: thesis: ( p,q,x are_collinear implies Mid x,p,f . x )

consider r being Element of OAS such that
A4: not p,q,r are_collinear by A3, DIRAF:37;
assume A5: p,q,x are_collinear ; :: thesis: Mid x,p,f . x
A6: ( x = p or not p,r,x are_collinear )

proof

A7: ( p,x,q are_collinear & p,x,p are_collinear ) by A5, DIRAF:30, DIRAF:31;
assume that
A8: x <> p and
A9: p,r,x are_collinear ; :: thesis: contradiction
p,x,r are_collinear by A9, DIRAF:30;
hence contradiction by A4, A8, A7, DIRAF:32; :: thesis: verum

end;

Mid r,p,f . r by A1, A2, A4, Th59;
hence Mid x,p,f . x by A1, A6, Th59, DIRAF:10; :: thesis: verum

end;

hence Mid x,p,f . x by A1, A2, Th59; :: thesis: verum