let SAS be Semi_Affine_Space; :: thesis: for a, b, c, o, p, q, 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, b, c, o, p, q, r be Element of SAS; :: thesis: ( trap a,p,b,q,o & trap a,p,c,r,o implies b,c // q,r )
assume that
A1: trap a,p,b,q,o and
A2: trap a,p,c,r,o ; :: thesis: b,c // q,r
not o,a,b are_collinear by A1;
then A3: not o,a // o,b ;
o,c,r are_collinear by A2;
then A4: o,c // o,r ;
not o,a,c are_collinear by A2;
then A5: not o,a // o,c ;
o,b,q are_collinear by A1;
then A6: o,b // o,q ;
o,a,p are_collinear by A1;
then A7: o,a // o,p ;
( a,b // p,q & a,c // p,r ) by A1, A2;
hence b,c // q,r by A3, A7, A6, A5, A4, Def1; :: thesis: verum