let SAS be Semi_Affine_Space; :: thesis: for a, a', b, b', c, c', d, d' being Element of SAS st parallelogram a,a',b,b' & parallelogram a,a',c,c' & parallelogram b,b',d,d' holds
c,d // c',d'
let a, a', b, b', c, c', d, d' be Element of SAS; :: thesis: ( parallelogram a,a',b,b' & parallelogram a,a',c,c' & parallelogram b,b',d,d' implies c,d // c',d' )
assume that
A1: parallelogram a,a',b,b' and
A2: parallelogram a,a',c,c' and
A3: parallelogram b,b',d,d' ; :: thesis: c,d // c',d'

A4: now

assume A5: not a,a',d is_collinear ; :: thesis: c,d // c',d'
parallelogram b,b',a,a' by A1, Th61;
then parallelogram a,a',d,d' by A3, A5, Th68;
hence c,d // c',d' by A2, Th67; :: thesis: verum

end;

A6: now

A7: ( not a,a',b is_collinear & a,a' // a,a' ) by A1, Th12, Th56;
A8: a <> a' by A1, Th54;
assume that
A9: b,b',c is_collinear and
A10: a,a',d is_collinear ; :: thesis: c,d // c',d'
a <> b by A1, Th54;
then consider x being Element of SAS such that
A11: a,b,x is_collinear and
A12: x <> a and
A13: x <> b by Th66;
a,b // a,x by A11, Def2;
then consider y being Element of SAS such that
A14: parallelogram a,a',x,y by A12, A7, A8, Th39, Th62;
A15: not x,y,d is_collinear by A10, A14, Th57;
parallelogram b,b',x,y by A1, A11, A13, A14, Th69;
then A16: parallelogram x,y,d,d' by A3, A15, Th68;
not x,y,c is_collinear by A1, A9, A11, A13, A14, Th57, Th69;
then parallelogram x,y,c,c' by A2, A14, Th68;
hence c,d // c',d' by A16, Th67; :: thesis: verum

end;

now

assume not b,b',c is_collinear ; :: thesis: c,d // c',d'
then parallelogram b,b',c,c' by A1, A2, Th68;
hence c,d // c',d' by A3, Th67; :: thesis: verum

end;

hence c,d // c',d' by A4, A6; :: thesis: verum