let FdSp be FanodesSp; :: thesis: for a, b, c, d, p, q, r, 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, b, c, d, p, q, r, 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 :: thesis: ( not a,p,d are_collinear implies c,d '||' r,s )

assume A5: not a,p,d are_collinear ; :: thesis: c,d '||' r,s
parallelogram b,q,a,p by A1, Th33;
then parallelogram a,p,d,s by A3, A5, Th40;
hence c,d '||' r,s by A2, Th39; :: thesis: verum

end;

A6: now :: thesis: ( b,q,c are_collinear & a,p,d are_collinear implies c,d '||' r,s )

A7: a <> p by A1, Th26;
A8: ( not a,p,b are_collinear & a,p '||' a,p ) by A1, PARSP_1:25;
assume that
A9: b,q,c are_collinear and
A10: a,p,d are_collinear ; :: thesis: c,d '||' r,s
a <> b by A1, Th26;
then consider x being Element of FdSp such that
A11: a,b,x are_collinear and
A12: x <> a and
A13: x <> b by Th38;
a,b '||' a,x by A11;
then consider y being Element of FdSp such that
A14: parallelogram a,p,x,y by A12, A8, A7, Th11, Th34;
A15: not x,y,d are_collinear by A10, A14, Th29;
parallelogram b,q,x,y by A1, A11, A13, A14, Th41;
then A16: parallelogram x,y,d,s by A3, A15, Th40;
not x,y,c are_collinear by A1, A9, A11, A13, A14, Th29, Th41;
then parallelogram x,y,c,r by A2, A14, Th40;
hence c,d '||' r,s by A16, Th39; :: thesis: verum

end;

now :: thesis: ( not b,q,c are_collinear implies c,d '||' r,s )

assume not b,q,c are_collinear ; :: thesis: c,d '||' r,s
then parallelogram b,q,c,r by A1, A2, Th40;
hence c,d '||' r,s by A3, Th39; :: thesis: verum

end;

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