let SAS be Semi_Affine_Space; for a, a9, b, b9, c, c9 being Element of SAS st a,b,c are_collinear & b <> c & 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; ( a,b,c are_collinear & b <> c & parallelogram a,a9,b,b9 & parallelogram a,a9,c,c9 implies parallelogram b,b9,c,c9 )
assume that
A1:
a,b,c are_collinear
and
A2:
b <> c
and
A3:
parallelogram a,a9,b,b9
and
A4:
parallelogram a,a9,c,c9
; parallelogram b,b9,c,c9
A5:
b <> b9
by A3, Th36;
a,b // a,c
by A1;
then A6:
a,b // b,c
by Th7;
thus
parallelogram b,b9,c,c9
by A2, A3, A4, A6, A5, Th23, Th50; verum