let SAS be Semi_Affine_Space; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum