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 holds
b,c // q,r
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 implies b,c // q,r )
assume ( trap a,p,b,q,o & trap a,p,c,r,o ) ; :: thesis: b,c // q,r
then ( not o,a,b is_collinear & o,a,p is_collinear & o,b,q is_collinear & a,b // p,q & not o,a,c is_collinear & o,c,r is_collinear & a,c // p,r ) by Def8;
then ( not o,a // o,b & o,a // o,p & o,b // o,q & a,b // p,q & not o,a // o,c & o,c // o,r & a,c // p,r ) by Def2;
hence b,c // q,r by Def1; :: thesis: verum