let o, p1, p2, p3, q1, q2, q3, r1, r2, r3 be Element of (ProjectiveSpace (TOP-REAL 3)); ( o <> p2 & o <> p3 & p2 <> p3 & p1 <> p2 & p1 <> p3 & o <> q2 & o <> q3 & q2 <> q3 & q1 <> q2 & q1 <> q3 & not o,p1,q1 are_collinear & o,p1,p2 are_collinear & o,p1,p3 are_collinear & o,q1,q2 are_collinear & o,q1,q3 are_collinear & p1,q2,r3 are_collinear & q1,p2,r3 are_collinear & p1,q3,r2 are_collinear & p3,q1,r2 are_collinear & p2,q3,r1 are_collinear & p3,q2,r1 are_collinear & p1,q1,r1 are_collinear implies r1,r2,r3 are_collinear )
assume that
A1:
( o <> p2 & o <> p3 & p2 <> p3 & p1 <> p2 & p1 <> p3 & o <> q2 & o <> q3 & q2 <> q3 & q1 <> q2 & q1 <> q3 & not o,p1,q1 are_collinear & o,p1,p2 are_collinear & o,p1,p3 are_collinear & o,q1,q2 are_collinear & o,q1,q3 are_collinear )
and
A2:
( p1,q2,r3 are_collinear & q1,p2,r3 are_collinear & p1,q3,r2 are_collinear & p3,q1,r2 are_collinear & p2,q3,r1 are_collinear & p3,q2,r1 are_collinear )
and
A3:
p1,q1,r1 are_collinear
; r1,r2,r3 are_collinear
per cases
( not p2,q2,r2 are_collinear or p2,q2,r2 are_collinear )
;
suppose A4:
not
p2,
q2,
r2 are_collinear
;
r1,r2,r3 are_collinear
(
o <> p1 &
o <> q1 &
o <> p3 &
p1 <> p3 &
p2 <> p1 &
p2 <> p3 &
o <> q3 &
q1 <> q3 &
q2 <> q1 &
q2 <> q3 & not
o,
p2,
q2 are_collinear &
o,
p2,
p1 are_collinear &
o,
p2,
p3 are_collinear &
o,
q2,
q1 are_collinear &
o,
q2,
q3 are_collinear &
p2,
q1,
r3 are_collinear &
q2,
p1,
r3 are_collinear &
p2,
q3,
r1 are_collinear &
p3,
q2,
r1 are_collinear &
p1,
q3,
r2 are_collinear &
p3,
q1,
r2 are_collinear )
by A1, A2, Th8, ANPROJ_2:24;
then
r2,
r1,
r3 are_collinear
by A4, Lm5;
hence
r1,
r2,
r3 are_collinear
by ANPROJ_2:24;
verum suppose A5:
p2,
q2,
r2 are_collinear
;
r1,r2,r3 are_collinear per cases
( not p3,q3,r3 are_collinear or p3,q3,r3 are_collinear )
;
suppose A6:
not
p3,
q3,
r3 are_collinear
;
r1,r2,r3 are_collinear
(
o <> p2 &
o <> p1 &
p2 <> p1 &
p3 <> p2 &
p3 <> p1 &
o <> q2 &
o <> q1 &
q2 <> q1 &
q3 <> q2 &
q3 <> q1 & not
o,
p3,
q3 are_collinear &
o,
p3,
p2 are_collinear &
o,
p3,
p1 are_collinear &
o,
q3,
q2 are_collinear &
o,
q3,
q1 are_collinear &
p3,
q2,
r1 are_collinear &
q3,
p2,
r1 are_collinear &
p3,
q1,
r2 are_collinear &
p1,
q3,
r2 are_collinear &
p2,
q1,
r3 are_collinear &
p1,
q2,
r3 are_collinear )
by A1, Th8, A2, COLLSP:4;
then
r3,
r2,
r1 are_collinear
by A6, Lm5;
hence
r1,
r2,
r3 are_collinear
by ANPROJ_2:24;
verum