let FdSp be FanodesSp; :: thesis: for o, a, b, x being Element of FdSp holds
( o,a,b is_collinear or not o,a,x is_collinear or not o,b,x is_collinear or o = x )
let o, a, b, x be Element of FdSp; :: thesis: ( o,a,b is_collinear or not o,a,x is_collinear or not o,b,x is_collinear or o = x )
assume A1: not o,a,b is_collinear ; :: thesis: ( not o,a,x is_collinear or not o,b,x is_collinear or o = x )

now

assume that
A2: o,a,x is_collinear and
A3: o,b,x is_collinear ; :: thesis: ( not o,a,x is_collinear or not o,b,x is_collinear or o = x )
a,o,x is_collinear by A2, Th15;
then A4: a,o '||' a,x by Def2;
b,o,x is_collinear by A3, Th15;
then A5: b,o '||' b,x by Def2;
not a,b,o is_collinear by A1, Th15;
then not a,b '||' a,o by Def2;
hence ( not o,a,x is_collinear or not o,b,x is_collinear or o = x ) by A4, A5, PARSP_1:33; :: thesis: verum

end;

hence ( not o,a,x is_collinear or not o,b,x is_collinear or o = x ) ; :: thesis: verum