let SAS be Semi_Affine_Space; for a, b, c, d, o being Element of SAS st o <> b & trap a,b,c,d,o holds
not o,b,d are_collinear
let a, b, c, d, o be Element of SAS; ( o <> b & trap a,b,c,d,o implies not o,b,d are_collinear )
assume that
A1:
o <> b
and
A2:
trap a,b,c,d,o
; not o,b,d are_collinear
o,a,b are_collinear
by A2;
then A3:
o,a // o,b
;
o,c,d are_collinear
by A2;
then A4:
o,c // o,d
;
( o <> d & not o,a,c are_collinear )
by A1, A2, Th94;
hence
not o,b,d are_collinear
by A1, A3, A4, Th23; verum