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 :: thesis: ( not a,a9,d are_collinear implies c,d // c9,d9 )
assume A5: not a,a9,d are_collinear ; :: thesis: c,d // c9,d9
parallelogram b,b9,a,a9 by A1, Th43;
then parallelogram a,a9,d,d9 by A3, A5, Th50;
hence c,d // c9,d9 by A2, Th49; :: thesis: verum
end;
A6: now :: thesis: ( b,b9,c are_collinear & a,a9,d are_collinear implies c,d // c9,d9 )
A7: ( not a,a9,b are_collinear & a,a9 // a,a9 ) by A1, Th1;
A8: a <> a9 by A1, Th36;
assume that
A9: b,b9,c are_collinear and
A10: a,a9,d are_collinear ; :: thesis: c,d // c9,d9
a <> b by A1, Th36;
then consider x being Element of SAS such that
A11: a,b,x are_collinear and
A12: x <> a and
A13: x <> b by Th48;
a,b // a,x by A11;
then consider y being Element of SAS such that
A14: parallelogram a,a9,x,y by A12, A7, A8, Th23, Th44;
A15: not x,y,d are_collinear by A10, A14, Th39;
parallelogram b,b9,x,y by A1, A11, A13, A14, Th51;
then A16: parallelogram x,y,d,d9 by A3, A15, Th50;
not x,y,c are_collinear by A1, A9, A11, A13, A14, Th39, Th51;
then parallelogram x,y,c,c9 by A2, A14, Th50;
hence c,d // c9,d9 by A16, Th49; :: thesis: verum
end;
now :: thesis: ( not b,b9,c are_collinear implies c,d // c9,d9 )
assume not b,b9,c are_collinear ; :: thesis: c,d // c9,d9
then parallelogram b,b9,c,c9 by A1, A2, Th50;
hence c,d // c9,d9 by A3, Th49; :: thesis: verum
end;
hence c,d // c9,d9 by A4, A6; :: thesis: verum