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 & not p,q,x are_collinear 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 & not p,q,x are_collinear 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 & not p,q,x are_collinear implies Mid x,p,f . x )
assume that
A1: f is dilatation and
A2: f . p = p and
A3: ( Mid q,p,f . q & not p,q,x are_collinear ) ; :: thesis: Mid x,p,f . x
q,x '||' f . q,f . x by A1, Th34;
then A4: q,x '||' f . x,f . q by DIRAF:22;
p,x '||' p,f . x by A1, A2, Th34;
then p,x,f . x are_collinear by DIRAF:def 5;
hence Mid x,p,f . x by A3, A4, PASCH:6; :: thesis: verum