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
A2: a,b // o,o by Def1;
( o,a,o is_collinear & o,b,o is_collinear ) by Th40;
hence trap a,o,b,o,o by A1, A2, Def8; :: thesis: verum