let FdSp be FanodesSp; :: thesis: for a, b, c, d being Element of FdSp st a <> b & a,b,c is_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 is_collinear & a,b '||' c,d implies a,c '||' b,d )
assume A1: ( a <> b & a,b,c is_collinear & a,b '||' c,d ) ; :: thesis: a,c '||' b,d

now

assume b <> c ; :: thesis: a,c '||' b,d
then ( b <> c & a,b '||' a,c ) by A1, Def2;
then ( b <> c & b,c '||' a,c & a,b '||' c,b ) by PARSP_1:41;
then ( b <> c & b,c '||' a,c & c,b '||' c,d ) by A1, PARSP_1:def 12;
then ( b <> c & b,c '||' a,c & b,c '||' b,d ) by PARSP_1:41;
hence a,c '||' b,d by PARSP_1:def 12; :: thesis: verum

end;

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