let SAS be Semi_Affine_Space; for a, b, c, x, y being Element of SAS st congr a,b,c,x & congr a,b,c,y holds
x = y
let a, b, c, x, y be Element of SAS; ( congr a,b,c,x & congr a,b,c,y implies x = y )
assume that
A1:
congr a,b,c,x
and
A2:
congr a,b,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, Th59;
hence
x = y
by Th45;
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
SAS such that A8:
parallelogram a,
b,
p,
q
by A6, Lm1;
parallelogram p,
q,
a,
b
by A8, Th43;
then
(
parallelogram p,
q,
c,
x &
parallelogram p,
q,
c,
y )
by A1, A2, A7, Th61;
hence
x = y
by Th45;
verum end;
now ( a = b implies x = y )end;
hence
x = y
by A5, A3; verum