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

A4: now

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

end;

A6: now

A7: ( not a,a9,b is_collinear & a,a9 // a,a9 ) by A1, Th12, Th56;
A8: a <> a9 by A1, Th54;
assume that
A9: b,b9,c is_collinear and
A10: a,a9,d is_collinear ; :: thesis: c,d // c9,d9
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,a9,x,y by A12, A7, A8, Th39, Th62;
A15: not x,y,d is_collinear by A10, A14, Th57;
parallelogram b,b9,x,y by A1, A11, A13, A14, Th69;
then A16: parallelogram x,y,d,d9 by A3, A15, Th68;
not x,y,c is_collinear by A1, A9, A11, A13, A14, Th57, Th69;
then parallelogram x,y,c,c9 by A2, A14, Th68;
hence c,d // c9,d9 by A16, Th67; :: thesis: verum

end;

now

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

end;

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