let SAS be Semi_Affine_Space; :: thesis: for a, b, c, d, o being Element of SAS st trap a,b,c,d,o holds
( o <> a & a <> c & c <> o )
let a, b, c, d, o be Element of SAS; :: thesis: ( trap a,b,c,d,o implies ( o <> a & a <> c & c <> o ) )
assume trap a,b,c,d,o ; :: thesis: ( o <> a & a <> c & c <> o )
then not o,a,c is_collinear by Def8;
hence ( o <> a & a <> c & c <> o ) by Th40; :: thesis: verum