let FdSp be FanodesSp; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum