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 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 is_collinear by A1, Def8;
then A3: not o,a // o,b by Def2;
o,c,r is_collinear by A2, Def8;
then A4: o,c // o,r by Def2;
not o,a,c is_collinear by A2, Def8;
then A5: not o,a // o,c by Def2;
o,b,q is_collinear by A1, Def8;
then A6: o,b // o,q by Def2;
o,a,p is_collinear by A1, Def8;
then A7: o,a // o,p by Def2;
( a,b // p,q & a,c // p,r ) by A1, A2, Def8;
hence b,c // q,r by A3, A7, A6, A5, A4, Def1; :: thesis: verum