let SAS be Semi_Affine_Space; :: thesis: for o, a, b being Element of SAS st not o,a,b is_collinear holds
trap a,o,b,o,o
let o, a, b be Element of SAS; :: thesis: ( not o,a,b is_collinear implies trap a,o,b,o,o )
assume A1: not o,a,b is_collinear ; :: thesis: trap a,o,b,o,o
( o,a,o is_collinear & o,b,o is_collinear & a,b // o,o ) by Def1, Th40;
hence trap a,o,b,o,o by A1, Def8; :: thesis: verum