let SAS be Semi_Affine_Space; 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; ( 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 ( not o,a,d are_collinear implies c,d // r,s )assume A5:
not
o,
a,
d are_collinear
;
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;
verum end;
A6:
now ( 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
;
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;
verum
A28:
now ( o = p implies c,d // r,s )assume A29:
o = p
;
c,d // r,sthen
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;
verum end;
now ( not o,b,c are_collinear implies c,d // r,s )assume
not
o,
b,
c are_collinear
;
c,d // r,sthen
trap b,
q,
c,
r,
o
by A1, A2, Th99;
hence
c,
d // r,
s
by A3, Th98;
verum end;
hence
c,d // r,s
by A4, A28, A6; verum