let SAS be Semi_Affine_Space; for a, p, b, q, o, c, r, d, 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, p, b, q, o, c, r, d, s be Element of SAS; ( 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
; c,d // r,s
A4:
now assume A5:
not
o,
a,
d is_collinear
;
c,d // r,s
trap b,
q,
a,
p,
o
by A1, Th121;
then
trap a,
p,
d,
s,
o
by A3, A5, Th127;
hence
c,
d // r,
s
by A2, Th126;
verum end;
A6:
now
not
o,
a,
b is_collinear
by A1, Def8;
then
not
b,
a,
o is_collinear
by Th37;
then consider x being
Element of
SAS such that A7:
parallelogram b,
a,
o,
x
by Th62;
o,
b,
q is_collinear
by A1, Def8;
then
o,
b // o,
q
by Def2;
then A8:
b,
o // q,
o
by Th17;
A9:
o,
x // o,
x
by Th12;
(
b,
o // a,
x &
b <> o )
by A7, Def3, Th54;
then A10:
q,
o // a,
x
by A8, Def1;
A11:
not
o,
x,
b is_collinear
by A7, Th56;
A12:
o <> d
by A3, Th118;
assume that A13:
o <> p
and A14:
o,
b,
c is_collinear
and A15:
o,
a,
d is_collinear
;
c,d // r,s
not
o,
p,
q is_collinear
by A1, A13, Th123;
then
not
q,
p,
o is_collinear
by Th37;
then consider y being
Element of
SAS such that A16:
parallelogram q,
p,
o,
y
by Th62;
A17:
not
o,
x,
a is_collinear
by A7, Th56;
A18:
o <> c
by A2, Th118;
a,
b // p,
q
by A1, Def8;
then A19:
b,
a // q,
p
by Th17;
A20:
o,
a,
p is_collinear
by A1, Def8;
(
b,
a // o,
x &
b <> a )
by A7, Def3, Th54;
then A21:
q,
p // o,
x
by A19, Def1;
A22:
o <> x
by A7, Th54;
(
q <> p &
q,
p // o,
y )
by A16, Def3, Th54;
then
o,
x // o,
y
by A21, Def1;
then A23:
o,
x,
y is_collinear
by Def2;
(
q,
o // p,
y &
q <> o )
by A16, Def3, Th54;
then A24:
a,
x // p,
y
by A10, Def1;
not
o,
a,
x is_collinear
by A7, Th56;
then A25:
trap a,
p,
x,
y,
o
by A23, A24, A20, Def8;
not
o,
b,
x is_collinear
by A7, Th56;
then A26:
trap b,
q,
x,
y,
o
by A1, A25, Th127;
o,
a // o,
d
by A15, Def2;
then A27:
trap x,
y,
d,
s,
o
by A3, A26, A22, A12, A17, A9, Th39, Th127;
o,
b // o,
c
by A14, Def2;
then
trap x,
y,
c,
r,
o
by A2, A25, A11, A22, A18, A9, Th39, Th127;
hence
c,
d // r,
s
by A27, Th126;
verum
A28:
now assume A29:
o = p
;
c,d // r,sthen
o = q
by A1, Th121, Th122;
then A30:
o = s
by A3, Th121, Th122;
o = r
by A2, A29, Th121, Th122;
hence
c,
d // r,
s
by A30, Def1;
verum end;
now assume
not
o,
b,
c is_collinear
;
c,d // r,sthen
trap b,
q,
c,
r,
o
by A1, A2, Th127;
hence
c,
d // r,
s
by A3, Th126;
verum end;
hence
c,d // r,s
by A4, A28, A6; verum