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 A1: ( parallelogram a,a',b,b' & parallelogram a,a',c,c' & parallelogram b,b',d,d' ) ; :: thesis: c,d // c',d'

A2: now

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

end;

A3: now

assume not a,a',d is_collinear ; :: thesis: c,d // c',d'
then ( not a,a',d is_collinear & parallelogram b,b',a,a' & parallelogram b,b',d,d' & parallelogram a,a',c,c' ) by A1, Th61;
then ( parallelogram a,a',d,d' & parallelogram a,a',c,c' ) by Th68;
hence c,d // c',d' by Th67; :: thesis: verum

end;

now

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

end;

hence c,d // c',d' by A2, A3; :: thesis: verum