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 )
then A2: x,y '||' f . x,f . y by Th51;
assume ( 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 & Mid y,p,f . y ) by A1, Th75;
then ( x,p // p,f . x & y,p // p,f . y ) by DIRAF:def 3;
hence ( LIN p,x,y or x,y // f . y,f . x ) by A2, PASCH:19; :: thesis: verum