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

now

assume c,d,x is_collinear ; :: thesis: ( not a,b,x is_collinear or not c,d,x is_collinear )
then c,d '||' c,x by Def2;
hence ( not a,b,x is_collinear or not c,d,x is_collinear ) by A1, Th22, PARSP_1:43; :: thesis: verum

end;

hence ( not a,b,x is_collinear or not c,d,x is_collinear ) ; :: thesis: verum