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

A3: now :: thesis: ( c <> d & a <> d implies not a,b,d are_collinear )

assume that
A4: c <> d and
A5: a <> d ; :: thesis: not a,b,d are_collinear
( a,c '||' c,a & c <> a ) by A1, PARSP_1:25;
then not c,d,a are_collinear by A1, A2, A4, Th11;
then A6: not d,c,a are_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 are_collinear by A5, A6, A7, Th11; :: thesis: verum

end;

a <> d by A1, A2, PARSP_1:23;
hence not a,b,d are_collinear by A1, A3; :: thesis: verum