let FdSp be FanodesSp; :: thesis: for a, p, b, q, c, r, d, s being Element of FdSp st parallelogram a,p,b,q & parallelogram a,p,c,r & parallelogram b,q,d,s holds
c,d '||' r,s
let a, p, b, q, c, r, d, s be Element of FdSp; :: thesis: ( parallelogram a,p,b,q & parallelogram a,p,c,r & parallelogram b,q,d,s implies c,d '||' r,s )
assume that
A1: parallelogram a,p,b,q and
A2: parallelogram a,p,c,r and
A3: parallelogram b,q,d,s ; :: thesis: c,d '||' r,s

A4: now

assume A5: not a,p,d is_collinear ; :: thesis: c,d '||' r,s
parallelogram b,q,a,p by A1, Th41;
then parallelogram a,p,d,s by A3, A5, Th48;
hence c,d '||' r,s by A2, Th47; :: thesis: verum

end;

A6: now

A7: a <> p by A1, Th34;
A8: ( not a,p,b is_collinear & a,p '||' a,p ) by A1, Th36, PARSP_1:42;
assume that
A9: b,q,c is_collinear and
A10: a,p,d is_collinear ; :: thesis: c,d '||' r,s
a <> b by A1, Th34;
then consider x being Element of FdSp such that
A11: a,b,x is_collinear and
A12: x <> a and
A13: x <> b by Th46;
a,b '||' a,x by A11, Def2;
then consider y being Element of FdSp such that
A14: parallelogram a,p,x,y by A12, A8, A7, Th17, Th42;
A15: not x,y,d is_collinear by A10, A14, Th37;
parallelogram b,q,x,y by A1, A11, A13, A14, Th49;
then A16: parallelogram x,y,d,s by A3, A15, Th48;
not x,y,c is_collinear by A1, A9, A11, A13, A14, Th37, Th49;
then parallelogram x,y,c,r by A2, A14, Th48;
hence c,d '||' r,s by A16, Th47; :: thesis: verum

end;

now

assume not b,q,c is_collinear ; :: thesis: c,d '||' r,s
then parallelogram b,q,c,r by A1, A2, Th48;
hence c,d '||' r,s by A3, Th47; :: thesis: verum

end;

hence c,d '||' r,s by A4, A6; :: thesis: verum