let OAS be OAffinSpace; for p, q, x being Element of OAS
for f being Permutation of the carrier of OAS st f is dilatation & f . p = p & Mid q,p,f . q & q <> p holds
Mid x,p,f . x
let p, q, x be Element of OAS; for f being Permutation of the carrier of OAS st f is dilatation & f . p = p & Mid q,p,f . q & q <> p holds
Mid x,p,f . x
let f be Permutation of the carrier of OAS; ( f is dilatation & f . p = p & Mid q,p,f . q & q <> p implies Mid x,p,f . x )
assume that
A1:
( f is dilatation & f . p = p )
and
A2:
Mid q,p,f . q
and
A3:
q <> p
; Mid x,p,f . x
now ( p,q,x are_collinear implies Mid x,p,f . x )consider r being
Element of
OAS such that A4:
not
p,
q,
r are_collinear
by A3, DIRAF:37;
assume A5:
p,
q,
x are_collinear
;
Mid x,p,f . xA6:
(
x = p or not
p,
r,
x are_collinear )
proof
A7:
(
p,
x,
q are_collinear &
p,
x,
p are_collinear )
by A5, DIRAF:30, DIRAF:31;
assume that A8:
x <> p
and A9:
p,
r,
x are_collinear
;
contradiction
p,
x,
r are_collinear
by A9, DIRAF:30;
hence
contradiction
by A4, A8, A7, DIRAF:32;
verum
end;
Mid r,
p,
f . r
by A1, A2, A4, Th59;
hence
Mid x,
p,
f . x
by A1, A6, Th59, DIRAF:10;
verum end;
hence
Mid x,p,f . x
by A1, A2, Th59; verum