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 ( not b,q,c is_collinear & parallelogram a,p,b,q & parallelogram a,p,c,r ) ; :: thesis: parallelogram b,q,c,r
then ( not b,q,c is_collinear & a <> p & a,p '||' b,q & a,p '||' c,r & b,c '||' q,r ) by Def3, Th34, Th47;
then ( not b,q,c is_collinear & b,q '||' c,r & b,c '||' q,r ) by PARSP_1:def 12;
hence parallelogram b,q,c,r by Def3; :: thesis: verum