let PCPP be Pappian CollProjectivePlane; :: thesis: for o, b1, a1, b2, a2, b3, a3, c3, c1, c2 being Element of PCPP st o <> b1 & a1 <> b1 & o <> b2 & a2 <> b2 & o <> b3 & a3 <> b3 & not o,a1,a2 is_collinear & not o,a1,a3 is_collinear & not o,a2,a3 is_collinear & a1,a2,c3 is_collinear & b1,b2,c3 is_collinear & a2,a3,c1 is_collinear & b2,b3,c1 is_collinear & a1,a3,c2 is_collinear & b1,b3,c2 is_collinear & o,a1,b1 is_collinear & o,a2,b2 is_collinear & o,a3,b3 is_collinear holds
c1,c2,c3 is_collinear
let o, b1, a1, b2, a2, b3, a3, c3, c1, c2 be Element of PCPP; :: thesis: ( o <> b1 & a1 <> b1 & o <> b2 & a2 <> b2 & o <> b3 & a3 <> b3 & not o,a1,a2 is_collinear & not o,a1,a3 is_collinear & not o,a2,a3 is_collinear & a1,a2,c3 is_collinear & b1,b2,c3 is_collinear & a2,a3,c1 is_collinear & b2,b3,c1 is_collinear & a1,a3,c2 is_collinear & b1,b3,c2 is_collinear & o,a1,b1 is_collinear & o,a2,b2 is_collinear & o,a3,b3 is_collinear implies c1,c2,c3 is_collinear )
assume that
A1: ( o <> b1 & a1 <> b1 & o <> b2 & a2 <> b2 & o <> b3 & a3 <> b3 & not o,a1,a2 is_collinear & not o,a1,a3 is_collinear ) and
A2: not o,a2,a3 is_collinear and
A3: ( a1,a2,c3 is_collinear & b1,b2,c3 is_collinear ) and
A4: a2,a3,c1 is_collinear and
A5: b2,b3,c1 is_collinear and
A6: ( a1,a3,c2 is_collinear & b1,b3,c2 is_collinear & o,a1,b1 is_collinear & o,a2,b2 is_collinear & o,a3,b3 is_collinear ) ; :: thesis: c1,c2,c3 is_collinear
A7: o <> c1 by A2, A4, Th3;
A8: b3,b2,c1 is_collinear by A5, Th3;
A9: ( not o,a3,a2 is_collinear & a3,a2,c1 is_collinear ) by A2, A4, Th3;

now

assume o,c1,c3 is_collinear ; :: thesis: c1,c2,c3 is_collinear
then A10: c1,c3,o is_collinear by Th3;
assume not c1,c2,c3 is_collinear ; :: thesis: contradiction
then A11: not c1,c3,c2 is_collinear by Th3;
then not c1,o,c2 is_collinear by A7, A10, Th8;
then not o,c1,c2 is_collinear by Th3;
hence contradiction by A1, A3, A6, A9, A8, A11, Lm3; :: thesis: verum

end;

hence c1,c2,c3 is_collinear by A1, A2, A3, A4, A5, A6, Lm3; :: thesis: verum