let FdSp be FanodesSp; for a, b, o, x being Element of FdSp holds
( o,a,b are_collinear or not o,a,x are_collinear or not o,b,x are_collinear or o = x )
let a, b, o, x be Element of FdSp; ( o,a,b are_collinear or not o,a,x are_collinear or not o,b,x are_collinear or o = x )
assume A1:
not o,a,b are_collinear
; ( not o,a,x are_collinear or not o,b,x are_collinear or o = x )
now ( o,a,x are_collinear & o,b,x are_collinear & o,a,x are_collinear & o,b,x are_collinear implies o = x )assume that A2:
o,
a,
x are_collinear
and A3:
o,
b,
x are_collinear
;
( not o,a,x are_collinear or not o,b,x are_collinear or o = x )
a,
o,
x are_collinear
by A2, Th10;
then A4:
a,
o '||' a,
x
;
b,
o,
x are_collinear
by A3, Th10;
then A5:
b,
o '||' b,
x
;
not
a,
b,
o are_collinear
by A1, Th10;
then
not
a,
b '||' a,
o
;
hence
( not
o,
a,
x are_collinear or not
o,
b,
x are_collinear or
o = x )
by A4, A5, PARSP_1:33;
verum end;
hence
( not o,a,x are_collinear or not o,b,x are_collinear or o = x )
; verum