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
(
o,
a,
x is_collinear &
o,
b,
x is_collinear )
;
:: thesis: ( not o,a,x is_collinear or not o,b,x is_collinear or o = x )then
( not
a,
b,
o is_collinear &
a,
o,
x is_collinear &
o,
b,
x is_collinear &
b,
o,
x is_collinear )
by A1, Th15;
then
( not
a,
b '||' a,
o &
a,
o '||' a,
x &
b,
o '||' b,
x )
by Def2;
hence
( not
o,
a,
x is_collinear or not
o,
b,
x is_collinear or
o = x )
by PARSP_1:51;
:: thesis: verum end;
hence
( not o,a,x is_collinear or not o,b,x is_collinear or o = x )
; :: thesis: verum