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 ( parallelogram a,b,c,d1 & parallelogram a,b,c,d2 ) ; :: thesis: d1 = d2
then ( not b,c,a is_collinear & a,b // c,d1 & a,c // b,d1 & a,b // c,d2 & a,c // b,d2 ) by Def3, Th56;
then ( not b,c // b,a & b,c // c,b & b,a // c,d1 & b,a // c,d2 & c,a // b,d1 & c,a // b,d2 ) by Def1, Def2, Th17;
hence d1 = d2 by Th33; :: thesis: verum