let FdSp be FanodesSp; :: thesis: for a, b, p, q, o being Element of FdSp st o <> a & o <> b & o,a,b are_collinear & o,a,p are_collinear & o,b,q are_collinear holds
a,b '||' p,q
let a, b, p, q, o be Element of FdSp; :: thesis: ( o <> a & o <> b & o,a,b are_collinear & o,a,p are_collinear & o,b,q are_collinear implies a,b '||' p,q )
assume that
A1: o <> a and
A2: o <> b and
A3: o,a,b are_collinear and
A4: o,a,p are_collinear and
A5: o,b,q are_collinear ; :: thesis: a,b '||' p,q

A6: now :: thesis: ( o <> p implies a,b '||' p,q )

A7: o,a '||' o,b by A3;
o,a '||' o,p by A4;
then A8: o,b '||' o,p by A1, A7, PARSP_1:def 12;
o,b '||' o,q by A5;
then o,p '||' o,q by A2, A8, PARSP_1:def 12;
then A9: o,p '||' p,q by PARSP_1:24;
o,b '||' a,b by A7, PARSP_1:24;
then A10: a,b '||' o,p by A2, A8, PARSP_1:def 12;
assume o <> p ; :: thesis: a,b '||' p,q
hence a,b '||' p,q by A10, A9, PARSP_1:26; :: thesis: verum

end;

now :: thesis: ( o = p implies a,b '||' p,q )

assume A11: o = p ; :: thesis: a,b '||' p,q
then p,a '||' p,b by A3;
then A12: a,b '||' p,b by PARSP_1:24;
p,b '||' p,q by A5, A11;
hence a,b '||' p,q by A2, A11, A12, PARSP_1:26; :: thesis: verum

end;

hence a,b '||' p,q by A6; :: thesis: verum