let FdSp be FanodesSp; :: thesis: for a, b, c, p, q, r being Element of FdSp st a,b,c are_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 are_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 are_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, Th26;
a,b '||' a,c by A1;
then A6: a,b '||' b,c by PARSP_1:24;
thus parallelogram b,q,c,r by A2, A3, A4, A5, A6, Th11, Th40; :: thesis: verum