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

A3: now

assume that
A4: c <> d and
A5: a <> d ; :: thesis: not a,b,d is_collinear
( a,c '||' c,a & c <> a ) by A1, Th18, PARSP_1:42;
then not c,d,a is_collinear by A1, A2, A4, Th17;
then A6: not d,c,a is_collinear by Th15;
A7: d,a '||' a,d by PARSP_1:42;
( a <> b & d,c '||' a,b ) by A1, A2, Th18, PARSP_1:40;
hence not a,b,d is_collinear by A5, A6, A7, Th17; :: thesis: verum

end;

now

assume a = d ; :: thesis: contradiction
then a,b '||' a,c by A2, PARSP_1:40;
hence contradiction by A1, Def2; :: thesis: verum

end;

hence not a,b,d is_collinear by A1, A3; :: thesis: verum