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

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

hence
f is negative_dilatation
; :: thesis: verum
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;( 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