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