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

now :: thesis: ( b <> c implies a,c '||' b,d )

A4: a,b '||' a,c by A2;
then a,b '||' c,b by PARSP_1:24;
then c,b '||' c,d by A1, A3, PARSP_1:def 12;
then A5: b,c '||' b,d by PARSP_1:24;
assume A6: b <> c ; :: thesis: a,c '||' b,d
b,c '||' a,c by A4, PARSP_1:24;
hence a,c '||' b,d by A6, A5, PARSP_1:def 12; :: thesis: verum

end;

hence a,c '||' b,d by A3; :: thesis: verum