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 ( o <> b & trap a,b,c,d,o ) ; :: thesis: not o,b,d is_collinear
then ( o <> b & o <> d & not o,a,c is_collinear & o,a,b is_collinear & o,c,d is_collinear ) by Def8, Th122;
then ( o <> b & o <> d & not o,a,c is_collinear & o,a // o,b & o,c // o,d ) by Def2;
hence not o,b,d is_collinear by Th39; :: thesis: verum