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