let SAS be Semi_Affine_Space; for b, b', c, a, a', c' being Element of 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 ; ( not b,b',c is_collinear & parallelogram a,a',b,b' & parallelogram a,a',c,c' implies parallelogram b,b',c,c' )
assume that
A1:
not b,b',c is_collinear
and
A2:
parallelogram a,a',b,b'
and
A3:
parallelogram a,a',c,c'
; parallelogram b,b',c,c'
A4:
a,a' // c,c'
by A3, Def3;
( a <> a' & a,a' // b,b' )
by A2, Def3, Th54;
then A5:
b,b' // c,c'
by A4, Def1;
b,c // b',c'
by A2, A3, Th67;
hence
parallelogram b,b',c,c'
by A1, A5, Def3; verum