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 :: thesis: ( c <> d & a <> d implies not a,b,d is_collinear )

assume that
A4: c <> d and
A5: a <> d ; :: thesis: not a,b,d is_collinear
( a,c '||' c,a & c <> a ) by A1, Th12, PARSP_1:25;
then not c,d,a is_collinear by A1, A2, A4, Th11;
then A6: not d,c,a is_collinear by Th10;
A7: d,a '||' a,d by PARSP_1:25;
( a <> b & d,c '||' a,b ) by A1, A2, Th12, PARSP_1:23;
hence not a,b,d is_collinear by A5, A6, A7, Th11; :: thesis: verum

end;

now :: thesis: not a = d

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

end;

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