let PCPP be CollProjectiveSpace; :: thesis: for a1, a2, b1, b2, o being Element of PCPP st not o,a1,a2 are_collinear & o,a1,b1 are_collinear & o,a2,b2 are_collinear & o <> b1 & o <> b2 holds
not o,b1,b2 are_collinear
let a1, a2, b1, b2, o be Element of PCPP; :: thesis: ( not o,a1,a2 are_collinear & o,a1,b1 are_collinear & o,a2,b2 are_collinear & o <> b1 & o <> b2 implies not o,b1,b2 are_collinear )
assume that
A1: ( not o,a1,a2 are_collinear & o,a1,b1 are_collinear ) and
A2: o,a2,b2 are_collinear and
A3: o <> b1 and
A4: o <> b2 ; :: thesis: not o,b1,b2 are_collinear
not o,b1,a2 are_collinear by A1, A3, Th6;
then not o,a2,b1 are_collinear by Th1;
then not o,b2,b1 are_collinear by A2, A4, Th6;
hence not o,b1,b2 are_collinear by Th1; :: thesis: verum