let SAS be Semi_Affine_Space; :: thesis: for a, p, b, q, o, c, r being Element of SAS st trap a,p,b,q,o & trap a,p,c,r,o & not o,b,c is_collinear holds
trap b,q,c,r,o
let a, p, b, q, o, c, r be Element of SAS; :: thesis: ( trap a,p,b,q,o & trap a,p,c,r,o & not o,b,c is_collinear implies trap b,q,c,r,o )
assume that
A1: ( trap a,p,b,q,o & trap a,p,c,r,o ) and
A2: not o,b,c is_collinear ; :: thesis: trap b,q,c,r,o
A3: b,c // q,r by A1, Th126;
( o,b,q is_collinear & o,c,r is_collinear ) by A1, Def8;
hence trap b,q,c,r,o by A2, A3, Def8; :: thesis: verum