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

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

proof

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

end;

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

end;

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