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 p,x,y are_collinear 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 p,x,y are_collinear 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 p,x,y are_collinear 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 p,x,y are_collinear or x,y // f . y,f . x )
assume A2: ( f . p = p & q <> p & Mid q,p,f . q ) ; :: thesis: ( p,x,y are_collinear or x,y // f . y,f . x )
then Mid x,p,f . x by A1, Th60;
then A3: x,p // p,f . x by DIRAF:def 3;
Mid y,p,f . y by A1, A2, Th60;
then A4: y,p // p,f . y by DIRAF:def 3;
x,y '||' f . x,f . y by A1, Th34;
hence ( p,x,y are_collinear or x,y // f . y,f . x ) by A3, A4, PASCH:12; :: thesis: verum