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