let S be satisfying_Tarski-model TarskiGeometryStruct ; for a, b, p being POINT of S holds
( reflection (b,(reflection (a,p))) = reflection (a,(reflection (b,p))) iff a = b )
let a, b, p be POINT of S; ( reflection (b,(reflection (a,p))) = reflection (a,(reflection (b,p))) iff a = b )
( reflection (b,(reflection (a,p))) = reflection (a,(reflection (b,p))) implies a = b )
proof
assume A1:
reflection (
b,
(reflection (a,p)))
= reflection (
a,
(reflection (b,p)))
;
a = b
set p9 =
reflection (
a,
p);
A2:
Middle p,
a,
reflection (
a,
p)
by DEFR;
Middle reflection (
b,
p),
a,
reflection (
b,
(reflection (a,p)))
by A1, DEFR;
then
Middle reflection (
b,
(reflection (b,p))),
reflection (
b,
a),
reflection (
b,
(reflection (b,(reflection (a,p)))))
by Satz7p15, Satz7p16;
then
Middle p,
reflection (
b,
a),
reflection (
b,
(reflection (b,(reflection (a,p)))))
by Satz7p7;
then
Middle p,
reflection (
b,
a),
reflection (
a,
p)
by Satz7p7;
hence
a = b
by A2, Satz7p17, Satz7p10;
verum
end;
hence
( reflection (b,(reflection (a,p))) = reflection (a,(reflection (b,p))) iff a = b )
; verum