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 & p1 <> q2 & 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 & p1 <> q2 & q2 <> q3 implies not p2,p1,q3 is_collinear )
assume A1: ( not p1,p2,q1 is_collinear & p1,p2,q2 is_collinear & q1,q2,q3 is_collinear & p1 <> q2 & q2 <> q3 ) ; :: thesis: not p2,p1,q3 is_collinear
assume A2: p2,p1,q3 is_collinear ; :: thesis: contradiction
A3: p1 <> p2 by A1, ANPROJ_2:def 7;
p1,p2,q3 is_collinear by A2, Th3;
then p1,q2,q3 is_collinear by A1, A3, Th4;
then A4: q2,q3,p1 is_collinear by Th3;
p2,p1,q2 is_collinear by A1, Th3;
then p2,q2,q3 is_collinear by A2, A3, Th4;
then A5: q2,q3,p2 is_collinear by Th3;
q2,q3,q1 is_collinear by A1, Th3;
hence contradiction by A1, A4, A5, ANPROJ_2:def 8; :: thesis: verum