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 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 & 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 )
; :: thesis: c1,c2,c3 is_collinear
then A2:
not o,a3,a2 is_collinear
by Th3;
A3:
( a3,a2,c1 is_collinear & b3,b2,c1 is_collinear )
by A1, Th3;
A4:
o <> c1
by A1, Th3;
now assume A5:
o,
c1,
c3 is_collinear
;
:: thesis: c1,c2,c3 is_collinear assume A6:
not
c1,
c2,
c3 is_collinear
;
:: thesis: contradictionthen A7:
not
c1,
c3,
c2 is_collinear
by Th3;
(
c1,
c3,
o is_collinear &
c1 <> c3 )
by A5, A6, Th3, ANPROJ_2:def 7;
then
not
c1,
o,
c2 is_collinear
by A4, A7, Th8;
then
not
o,
c1,
c2 is_collinear
by Th3;
hence
contradiction
by A1, A2, A3, A7, Lm3;
:: thesis: verum end;
hence
c1,c2,c3 is_collinear
by A1, Lm3; :: thesis: verum