let OAS be OAffinSpace; :: thesis: for p, q 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 holds
f is negative_dilatation
let p, q 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 holds
f is negative_dilatation
let f be Permutation of the carrier of OAS; :: thesis: ( f is dilatation & f . p = p & q <> p & Mid q,p,f . q implies f is negative_dilatation )
assume A1: ( f is dilatation & f . p = p & q <> p & Mid q,p,f . q ) ; :: thesis: f is negative_dilatation
for x, y being Element of OAS holds x,y // f . y,f . x

proof

let x, y be Element of OAS; :: thesis: x,y // f . y,f . x
( not p,x,y are_collinear implies x,y // f . y,f . x ) by A1, Th61;
hence x,y // f . y,f . x by A1, Th62; :: thesis: verum

end;

hence f is negative_dilatation ; :: thesis: verum