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 that
A1: a,b,c is_collinear and
A2: b <> c and
A3: parallelogram a,p,b,q and
A4: parallelogram a,p,c,r ; :: thesis: parallelogram b,q,c,r
A5: b <> q by A3, Th34;
a,b '||' a,c by A1, Def2;
then A6: a,b '||' b,c by PARSP_1:24;
( not a,p,b is_collinear & a,p '||' b,q ) by A3, Def3;
hence parallelogram b,q,c,r by A2, A3, A4, A5, A6, Th17, Th48; :: thesis: verum