let PCPP be CollProjectiveSpace; 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; ( 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
; 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; verum