let FdSp be FanodesSp; for a, b, c, x, y being Element of FdSp st a,b congr c,x & a,b congr c,y holds
x = y
let a, b, c, x, y be Element of FdSp; ( a,b congr c,x & a,b congr c,y implies x = y )
assume that
A1:
a,b congr c,x
and
A2:
a,b congr c,y
; x = y
A3:
now ( a <> b & not a,b,c are_collinear implies x = y )assume that
a <> b
and A4:
not
a,
b,
c are_collinear
;
x = y
(
parallelogram a,
b,
c,
x &
parallelogram a,
b,
c,
y )
by A1, A2, A4, Th50;
hence
x = y
by Th35;
verum end;
A5:
now ( a <> b & a,b,c are_collinear implies x = y )assume that A6:
a <> b
and A7:
a,
b,
c are_collinear
;
x = yconsider p,
q being
Element of
FdSp such that A8:
parallelogram a,
b,
p,
q
by A6, Th43;
parallelogram p,
q,
a,
b
by A8, Th33;
then
(
parallelogram p,
q,
c,
x &
parallelogram p,
q,
c,
y )
by A1, A2, A7, Th52;
hence
x = y
by Th35;
verum end;
now ( a = b implies x = y )end;
hence
x = y
by A5, A3; verum