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