let SAS be Semi_Affine_Space; for a, b, c, d1, d2 being Element of SAS st parallelogram a,b,c,d1 & parallelogram a,b,c,d2 holds
d1 = d2
let a, b, c, d1, d2 be Element of SAS; ( parallelogram a,b,c,d1 & parallelogram a,b,c,d2 implies d1 = d2 )
assume that
A1:
parallelogram a,b,c,d1
and
A2:
parallelogram a,b,c,d2
; d1 = d2
not b,c,a are_collinear
by A1, Th38;
then A3:
not b,c // b,a
;
a,c // b,d2
by A2;
then A4:
c,a // b,d2
by Th6;
a,b // c,d2
by A2;
then A5:
b,a // c,d2
by Th6;
a,c // b,d1
by A1;
then A6:
c,a // b,d1
by Th6;
a,b // c,d1
by A1;
then A7:
b,a // c,d1
by Th6;
b,c // c,b
by Def1;
hence
d1 = d2
by A3, A7, A5, A6, A4, Th19; verum