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