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