let SAS be Semi_Affine_Space; :: thesis: for a, a9, b, b9, c, c9 being Element of SAS st not b,b9,c are_collinear & parallelogram a,a9,b,b9 & parallelogram a,a9,c,c9 holds
parallelogram b,b9,c,c9
let a, a9, b, b9, c, c9 be Element of SAS; :: thesis: ( not b,b9,c are_collinear & parallelogram a,a9,b,b9 & parallelogram a,a9,c,c9 implies parallelogram b,b9,c,c9 )
assume that
A1: not b,b9,c are_collinear and
A2: parallelogram a,a9,b,b9 and
A3: parallelogram a,a9,c,c9 ; :: thesis: parallelogram b,b9,c,c9
A4: a,a9 // c,c9 by A3;
( a <> a9 & a,a9 // b,b9 ) by A2, Th36;
then A5: b,b9 // c,c9 by A4, Def1;
b,c // b9,c9 by A2, A3, Th49;
hence parallelogram b,b9,c,c9 by A1, A5; :: thesis: verum