let OAS be OAffinSpace; :: thesis: for p, q, x, y being Element of OAS
for f being Permutation of the carrier of OAS st f is dilatation & f . p = p & q <> p & Mid q,p,f . q & not LIN p,x,y holds
x,y // f . y,f . x
let p, q, x, y be Element of OAS; :: thesis: for f being Permutation of the carrier of OAS st f is dilatation & f . p = p & q <> p & Mid q,p,f . q & not LIN p,x,y holds
x,y // f . y,f . x
let f be Permutation of the carrier of OAS; :: thesis: ( f is dilatation & f . p = p & q <> p & Mid q,p,f . q & not LIN p,x,y implies x,y // f . y,f . x )
assume A1: f is dilatation ; :: thesis: ( not f . p = p or not q <> p or not Mid q,p,f . q or LIN p,x,y or x,y // f . y,f . x )
assume A2: ( f . p = p & q <> p & Mid q,p,f . q ) ; :: thesis: ( LIN p,x,y or x,y // f . y,f . x )
then Mid x,p,f . x by A1, Th75;
then A3: x,p // p,f . x by DIRAF:def 3;
Mid y,p,f . y by A1, A2, Th75;
then A4: y,p // p,f . y by DIRAF:def 3;
x,y '||' f . x,f . y by A1, Th51;
hence ( LIN p,x,y or x,y // f . y,f . x ) by A3, A4, PASCH:12; :: thesis: verum