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

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