let FdSp be FanodesSp; for a, b, c, p, q, r being Element of FdSp st not b,q,c are_collinear & parallelogram a,p,b,q & parallelogram a,p,c,r holds
parallelogram b,q,c,r
let a, b, c, p, q, r be Element of FdSp; ( not b,q,c are_collinear & parallelogram a,p,b,q & parallelogram a,p,c,r implies parallelogram b,q,c,r )
assume that
A1:
not b,q,c are_collinear
and
A2:
parallelogram a,p,b,q
and
A3:
parallelogram a,p,c,r
; parallelogram b,q,c,r
A4:
a,p '||' c,r
by A3;
( a <> p & a,p '||' b,q )
by A2, Th26;
then A5:
b,q '||' c,r
by A4, PARSP_1:def 12;
b,c '||' q,r
by A2, A3, Th39;
hence
parallelogram b,q,c,r
by A1, A5; verum