let SAS be Semi_Affine_Space; :: thesis: for a, b, c, a', b', c' being Element of SAS st a,b,c is_collinear & b <> c & parallelogram a,a',b,b' & parallelogram a,a',c,c' holds
parallelogram b,b',c,c'
let a, b, c, a', b', c' be Element of SAS; :: thesis: ( a,b,c is_collinear & b <> c & parallelogram a,a',b,b' & parallelogram a,a',c,c' implies parallelogram b,b',c,c' )
assume that
A1: a,b,c is_collinear and
A2: b <> c and
A3: parallelogram a,a',b,b' and
A4: parallelogram a,a',c,c' ; :: thesis: parallelogram b,b',c,c'
A5: b <> b' by A3, Th54;
a,b // a,c by A1, Def2;
then A6: a,b // b,c by Th18;
( not a,a',b is_collinear & a,a' // b,b' ) by A3, Def3;
hence parallelogram b,b',c,c' by A2, A3, A4, A6, A5, Th39, Th68; :: thesis: verum