let SAS be Semi_Affine_Space; :: thesis: for a, b, c, d, o, p, q, r, s being Element of SAS st trap a,p,b,q,o & trap a,p,c,r,o & trap b,q,d,s,o holds
c,d // r,s
let a, b, c, d, o, p, q, r, s be Element of SAS; :: thesis: ( trap a,p,b,q,o & trap a,p,c,r,o & trap b,q,d,s,o implies c,d // r,s )
assume that
A1: trap a,p,b,q,o and
A2: trap a,p,c,r,o and
A3: trap b,q,d,s,o ; :: thesis: c,d // r,s

A4: now :: thesis: ( not o,a,d are_collinear implies c,d // r,s )

assume A5: not o,a,d are_collinear ; :: thesis: c,d // r,s
trap b,q,a,p,o by A1, Th93;
then trap a,p,d,s,o by A3, A5, Th99;
hence c,d // r,s by A2, Th98; :: thesis: verum

end;

A6: now :: thesis: ( o <> p & o,b,c are_collinear & o,a,d are_collinear implies c,d // r,s )

not o,a,b are_collinear by A1;
then not b,a,o are_collinear by Th22;
then consider x being Element of SAS such that
A7: parallelogram b,a,o,x by Th44;
o,b,q are_collinear by A1;
then o,b // o,q ;
then A8: b,o // q,o by Th6;
A9: o,x // o,x by Th1;
( b,o // a,x & b <> o ) by A7, Th36;
then A10: q,o // a,x by A8, Def1;
A11: not o,x,b are_collinear by A7, Th38;
A12: o <> d by A3, Th90;
assume that
A13: o <> p and
A14: o,b,c are_collinear and
A15: o,a,d are_collinear ; :: thesis: c,d // r,s
not o,p,q are_collinear by A1, A13, Th95;
then not q,p,o are_collinear by Th22;
then consider y being Element of SAS such that
A16: parallelogram q,p,o,y by Th44;
A17: not o,x,a are_collinear by A7, Th38;
A18: o <> c by A2, Th90;
a,b // p,q by A1;
then A19: b,a // q,p by Th6;
A20: o,a,p are_collinear by A1;
( b,a // o,x & b <> a ) by A7, Th36;
then A21: q,p // o,x by A19, Def1;
A22: o <> x by A7, Th36;
( q <> p & q,p // o,y ) by A16, Th36;
then o,x // o,y by A21, Def1;
then A23: o,x,y are_collinear ;
( q,o // p,y & q <> o ) by A16, Th36;
then A24: a,x // p,y by A10, Def1;
not o,a,x are_collinear by A7, Th38;
then A25: trap a,p,x,y,o by A23, A24, A20;
not o,b,x are_collinear by A7, Th38;
then A26: trap b,q,x,y,o by A1, A25, Th99;
o,a // o,d by A15;
then A27: trap x,y,d,s,o by A3, A26, A22, A12, A17, A9, Th23, Th99;
o,b // o,c by A14;
then trap x,y,c,r,o by A2, A25, A11, A22, A18, A9, Th23, Th99;
hence c,d // r,s by A27, Th98; :: thesis: verum

end;

A28: now :: thesis: ( o = p implies c,d // r,s )

assume A29: o = p ; :: thesis: c,d // r,s
then o = q by A1, Th93, Th94;
then A30: o = s by A3, Th93, Th94;
o = r by A2, A29, Th93, Th94;
hence c,d // r,s by A30, Def1; :: thesis: verum

end;

now :: thesis: ( not o,b,c are_collinear implies c,d // r,s )

assume not o,b,c are_collinear ; :: thesis: c,d // r,s
then trap b,q,c,r,o by A1, A2, Th99;
hence c,d // r,s by A3, Th98; :: thesis: verum

end;

hence c,d // r,s by A4, A28, A6; :: thesis: verum