let OAS be OAffinSpace; 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; 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; ( 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 )
; 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;
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;
verum
end;
hence
f is negative_dilatation
; verum