let PCPP be CollProjectiveSpace; :: thesis: for p1, p2, q1, p3, q2 being Element of PCPP st not p1,p2,q1 is_collinear & p1,p2,p3 is_collinear & q1,q2,p1 is_collinear & p1 <> p3 & p1 <> q2 holds
not p3,p1,q2 is_collinear
let p1, p2, q1, p3, q2 be Element of PCPP; :: thesis: ( not p1,p2,q1 is_collinear & p1,p2,p3 is_collinear & q1,q2,p1 is_collinear & p1 <> p3 & p1 <> q2 implies not p3,p1,q2 is_collinear )
assume A1: ( not p1,p2,q1 is_collinear & p1,p2,p3 is_collinear & q1,q2,p1 is_collinear & p1 <> p3 & p1 <> q2 ) ; :: thesis: not p3,p1,q2 is_collinear
assume p3,p1,q2 is_collinear ; :: thesis: contradiction
then ( p1,p3,q2 is_collinear & p1,p3,p2 is_collinear ) by A1, Th3;
then A2: p1,q2,p2 is_collinear by A1, Th4;
p1,q2,q1 is_collinear by A1, Th3;
hence contradiction by A1, A2, Th4; :: thesis: verum