let PCPP be CollProjectiveSpace; for p1, p2, q1, q2, q3 being Element of PCPP st not p1,p2,q1 are_collinear & p1,p2,q2 are_collinear & q1,q2,q3 are_collinear & q2 <> q3 holds
not p2,p1,q3 are_collinear
let p1, p2, q1, q2, q3 be Element of PCPP; ( not p1,p2,q1 are_collinear & p1,p2,q2 are_collinear & q1,q2,q3 are_collinear & q2 <> q3 implies not p2,p1,q3 are_collinear )
assume that
A1:
not p1,p2,q1 are_collinear
and
A2:
p1,p2,q2 are_collinear
and
A3:
q1,q2,q3 are_collinear
and
A4:
q2 <> q3
; not p2,p1,q3 are_collinear
A5:
p1 <> p2
by A1, ANPROJ_2:def 7;
assume A6:
p2,p1,q3 are_collinear
; contradiction
then
p1,p2,q3 are_collinear
by Th1;
then
p1,q2,q3 are_collinear
by A2, A5, Th2;
then A7:
q2,q3,p1 are_collinear
by Th1;
p2,p1,q2 are_collinear
by A2, Th1;
then
p2,q2,q3 are_collinear
by A6, A5, Th2;
then A8:
q2,q3,p2 are_collinear
by Th1;
q2,q3,q1 are_collinear
by A3, Th1;
hence
contradiction
by A1, A4, A7, A8, ANPROJ_2:def 8; verum