let FdSp be FanodesSp; :: thesis: for a, b, c, p, q, r being Element of FdSp st a,b,c is_collinear & b <> c & 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: ( a,b,c is_collinear & b <> c & parallelogram a,p,b,q & parallelogram a,p,c,r implies parallelogram b,q,c,r )
assume ( a,b,c is_collinear & b <> c & parallelogram a,p,b,q & parallelogram a,p,c,r ) ; :: thesis: parallelogram b,q,c,r
then ( a,b '||' a,c & not a,p,b is_collinear & a,p '||' b,q & b <> q & b <> c & parallelogram a,p,b,q & parallelogram a,p,c,r ) by Def2, Def3, Th34;
then ( not a,p,b is_collinear & a,p '||' b,q & b <> q & b <> c & a,b '||' b,c & parallelogram a,p,b,q & parallelogram a,p,c,r ) by PARSP_1:41;
hence parallelogram b,q,c,r by Th17, Th48; :: thesis: verum