let SAS be Semi_Affine_Space; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum