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 LIN p,q,x 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 LIN p,q,x 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 LIN p,q,x implies Mid x,p,f . x )
assume that
A1: f is dilatation and
A2: f . p = p and
A3: Mid q,p,f . q and
A4: not LIN p,q,x ; :: thesis: Mid x,p,f . x
p,x '||' p,f . x by A1, A2, Th51;
then A5: LIN p,x,f . x by DIRAF:def 5;
q,x '||' f . q,f . x by A1, Th51;
then q,x '||' f . x,f . q by DIRAF:27;
hence Mid x,p,f . x by A3, A4, A5, PASCH:13; :: thesis: verum