let SAS be Semi_Affine_Space; :: thesis: for b, b', c, a, a', c' being Element of SAS st not b,b',c is_collinear & parallelogram a,a',b,b' & parallelogram a,a',c,c' holds
parallelogram b,b',c,c'
let b, b', c, a, a', c' be Element of SAS; :: thesis: ( not b,b',c is_collinear & parallelogram a,a',b,b' & parallelogram a,a',c,c' implies parallelogram b,b',c,c' )
assume ( not b,b',c is_collinear & parallelogram a,a',b,b' & parallelogram a,a',c,c' ) ; :: thesis: parallelogram b,b',c,c'
then ( not b,b',c is_collinear & a <> a' & a,a' // b,b' & a,a' // c,c' & b,c // b',c' ) by Def3, Th54, Th67;
then ( not b,b',c is_collinear & b,b' // c,c' & b,c // b',c' ) by Def1;
hence parallelogram b,b',c,c' by Def3; :: thesis: verum