:: HESSENBE semantic presentation begin theorem Th1: :: HESSENBE:1 for PCPP being CollProjectiveSpace for a, b, c being Element of PCPP st a,b,c is_collinear holds ( b,c,a is_collinear & c,a,b is_collinear & b,a,c is_collinear & a,c,b is_collinear & c,b,a is_collinear ) proof let PCPP be CollProjectiveSpace; ::_thesis: for a, b, c being Element of PCPP st a,b,c is_collinear holds ( b,c,a is_collinear & c,a,b is_collinear & b,a,c is_collinear & a,c,b is_collinear & c,b,a is_collinear ) let a, b, c be Element of PCPP; ::_thesis: ( a,b,c is_collinear implies ( b,c,a is_collinear & c,a,b is_collinear & b,a,c is_collinear & a,c,b is_collinear & c,b,a is_collinear ) ) assume A1: a,b,c is_collinear ; ::_thesis: ( b,c,a is_collinear & c,a,b is_collinear & b,a,c is_collinear & a,c,b is_collinear & c,b,a is_collinear ) then b,a,c is_collinear by COLLSP:4; then A2: b,c,a is_collinear by COLLSP:4; a,c,b is_collinear by A1, COLLSP:4; hence ( b,c,a is_collinear & c,a,b is_collinear & b,a,c is_collinear & a,c,b is_collinear & c,b,a is_collinear ) by A2, COLLSP:4; ::_thesis: verum end; theorem Th2: :: HESSENBE:2 for PCPP being CollProjectiveSpace for a, b, c, d being Element of PCPP st a <> b & a,b,c is_collinear & a,b,d is_collinear holds a,c,d is_collinear proof let PCPP be CollProjectiveSpace; ::_thesis: for a, b, c, d being Element of PCPP st a <> b & a,b,c is_collinear & a,b,d is_collinear holds a,c,d is_collinear let a, b, c, d be Element of PCPP; ::_thesis: ( a <> b & a,b,c is_collinear & a,b,d is_collinear implies a,c,d is_collinear ) A1: a,b,a is_collinear by ANPROJ_2:def_7; assume ( a <> b & a,b,c is_collinear & a,b,d is_collinear ) ; ::_thesis: a,c,d is_collinear hence a,c,d is_collinear by A1, ANPROJ_2:def_8; ::_thesis: verum end; theorem :: HESSENBE:3 for PCPP being CollProjectiveSpace for p, q, a, b, r being Element of PCPP st p <> q & a,b,p is_collinear & a,b,q is_collinear & p,q,r is_collinear holds a,b,r is_collinear proof let PCPP be CollProjectiveSpace; ::_thesis: for p, q, a, b, r being Element of PCPP st p <> q & a,b,p is_collinear & a,b,q is_collinear & p,q,r is_collinear holds a,b,r is_collinear let p, q, a, b, r be Element of PCPP; ::_thesis: ( p <> q & a,b,p is_collinear & a,b,q is_collinear & p,q,r is_collinear implies a,b,r is_collinear ) assume that A1: p <> q and A2: ( a,b,p is_collinear & a,b,q is_collinear ) and A3: p,q,r is_collinear ; ::_thesis: a,b,r is_collinear now__::_thesis:_(_a_<>_b_implies_a,b,r_is_collinear_) assume A4: a <> b ; ::_thesis: a,b,r is_collinear ( b,a,p is_collinear & b,a,q is_collinear ) by A2, Th1; then b,p,q is_collinear by A4, Th2; then A5: p,q,b is_collinear by Th1; a,p,q is_collinear by A2, A4, Th2; then p,q,a is_collinear by Th1; hence a,b,r is_collinear by A1, A3, A5, ANPROJ_2:def_8; ::_thesis: verum end; hence a,b,r is_collinear by ANPROJ_2:def_7; ::_thesis: verum end; theorem Th4: :: HESSENBE:4 for PCPP being CollProjectiveSpace for p, q being Element of PCPP st p <> q holds ex r being Element of PCPP st not p,q,r is_collinear proof let PCPP be CollProjectiveSpace; ::_thesis: for p, q being Element of PCPP st p <> q holds ex r being Element of PCPP st not p,q,r is_collinear let p, q be Element of PCPP; ::_thesis: ( p <> q implies ex r being Element of PCPP st not p,q,r is_collinear ) consider a, b, c being Element of PCPP such that A1: not a,b,c is_collinear by COLLSP:def_6; assume p <> q ; ::_thesis: not for r being Element of PCPP holds p,q,r is_collinear then ( p,q,a is_collinear & p,q,b is_collinear implies not p,q,c is_collinear ) by A1, ANPROJ_2:def_8; hence not for r being Element of PCPP holds p,q,r is_collinear ; ::_thesis: verum end; theorem :: HESSENBE:5 for PCPP being CollProjectiveSpace for p being Element of PCPP holds not for q, r being Element of PCPP holds p,q,r is_collinear proof let PCPP be CollProjectiveSpace; ::_thesis: for p being Element of PCPP holds not for q, r being Element of PCPP holds p,q,r is_collinear let p be Element of PCPP; ::_thesis: not for q, r being Element of PCPP holds p,q,r is_collinear consider q being Element of PCPP such that A1: p <> q and p <> q and p,p,q is_collinear by ANPROJ_2:def_10; not for r being Element of PCPP holds p,q,r is_collinear by A1, Th4; hence not for q, r being Element of PCPP holds p,q,r is_collinear ; ::_thesis: verum end; theorem Th6: :: HESSENBE:6 for PCPP being CollProjectiveSpace for a, b, c, b9 being Element of PCPP st not a,b,c is_collinear & a,b,b9 is_collinear & a <> b9 holds not a,b9,c is_collinear proof let PCPP be CollProjectiveSpace; ::_thesis: for a, b, c, b9 being Element of PCPP st not a,b,c is_collinear & a,b,b9 is_collinear & a <> b9 holds not a,b9,c is_collinear let a, b, c, b9 be Element of PCPP; ::_thesis: ( not a,b,c is_collinear & a,b,b9 is_collinear & a <> b9 implies not a,b9,c is_collinear ) assume that A1: not a,b,c is_collinear and A2: a,b,b9 is_collinear and A3: a <> b9 ; ::_thesis: not a,b9,c is_collinear assume A4: a,b9,c is_collinear ; ::_thesis: contradiction a,b9,b is_collinear by A2, Th1; hence contradiction by A1, A3, A4, Th2; ::_thesis: verum end; theorem Th7: :: HESSENBE:7 for PCPP being CollProjectiveSpace for a, b, c, d being Element of PCPP st not a,b,c is_collinear & a,b,d is_collinear & a,c,d is_collinear holds a = d proof let PCPP be CollProjectiveSpace; ::_thesis: for a, b, c, d being Element of PCPP st not a,b,c is_collinear & a,b,d is_collinear & a,c,d is_collinear holds a = d let a, b, c, d be Element of PCPP; ::_thesis: ( not a,b,c is_collinear & a,b,d is_collinear & a,c,d is_collinear implies a = d ) assume that A1: not a,b,c is_collinear and A2: ( a,b,d is_collinear & a,c,d is_collinear ) ; ::_thesis: a = d assume A3: not a = d ; ::_thesis: contradiction A4: a,d,a is_collinear by ANPROJ_2:def_7; ( a,d,b is_collinear & a,d,c is_collinear ) by A2, Th1; hence contradiction by A1, A3, A4, ANPROJ_2:def_8; ::_thesis: verum end; theorem Th8: :: HESSENBE:8 for PCPP being CollProjectiveSpace for o, a, d, d9, a9, x being Element of PCPP st not o,a,d is_collinear & o,d,d9 is_collinear & d <> d9 & a9,d9,x is_collinear & o,a,a9 is_collinear & o <> a9 holds x <> d proof let PCPP be CollProjectiveSpace; ::_thesis: for o, a, d, d9, a9, x being Element of PCPP st not o,a,d is_collinear & o,d,d9 is_collinear & d <> d9 & a9,d9,x is_collinear & o,a,a9 is_collinear & o <> a9 holds x <> d let o, a, d, d9, a9, x be Element of PCPP; ::_thesis: ( not o,a,d is_collinear & o,d,d9 is_collinear & d <> d9 & a9,d9,x is_collinear & o,a,a9 is_collinear & o <> a9 implies x <> d ) assume that A1: not o,a,d is_collinear and A2: o,d,d9 is_collinear and A3: d <> d9 and A4: a9,d9,x is_collinear and A5: o,a,a9 is_collinear and A6: o <> a9 ; ::_thesis: x <> d assume not x <> d ; ::_thesis: contradiction then A7: d,d9,a9 is_collinear by A4, Th1; d,d9,o is_collinear by A2, Th1; then d,o,a9 is_collinear by A3, A7, Th2; then A8: o,a9,d is_collinear by Th1; o,a9,a is_collinear by A5, Th1; hence contradiction by A1, A6, A8, Th2; ::_thesis: verum end; theorem Th9: :: HESSENBE:9 for PCPP being CollProjectiveSpace for a1, a2, a3, c3, c1, x being Element of PCPP st not a1,a2,a3 is_collinear & a1,a2,c3 is_collinear & a2,a3,c1 is_collinear & c1,c3,x is_collinear & c3 <> a1 & c3 <> a2 & c1 <> a2 & c1 <> a3 holds ( a1 <> x & a3 <> x ) proof let PCPP be CollProjectiveSpace; ::_thesis: for a1, a2, a3, c3, c1, x being Element of PCPP st not a1,a2,a3 is_collinear & a1,a2,c3 is_collinear & a2,a3,c1 is_collinear & c1,c3,x is_collinear & c3 <> a1 & c3 <> a2 & c1 <> a2 & c1 <> a3 holds ( a1 <> x & a3 <> x ) let a1, a2, a3, c3, c1, x be Element of PCPP; ::_thesis: ( not a1,a2,a3 is_collinear & a1,a2,c3 is_collinear & a2,a3,c1 is_collinear & c1,c3,x is_collinear & c3 <> a1 & c3 <> a2 & c1 <> a2 & c1 <> a3 implies ( a1 <> x & a3 <> x ) ) assume that A1: not a1,a2,a3 is_collinear and A2: a1,a2,c3 is_collinear and A3: a2,a3,c1 is_collinear and A4: c1,c3,x is_collinear and A5: c3 <> a1 and A6: c3 <> a2 and A7: c1 <> a2 and A8: c1 <> a3 ; ::_thesis: ( a1 <> x & a3 <> x ) A9: a3 <> x proof assume not a3 <> x ; ::_thesis: contradiction then A10: a3,c1,c3 is_collinear by A4, Th1; a3,c1,a2 is_collinear by A3, Th1; then a3,a2,c3 is_collinear by A8, A10, Th2; then A11: a2,c3,a3 is_collinear by Th1; a2,c3,a1 is_collinear by A2, Th1; then a2,a1,a3 is_collinear by A6, A11, Th2; hence contradiction by A1, Th1; ::_thesis: verum end; a1 <> x proof assume not a1 <> x ; ::_thesis: contradiction then A12: a1,c3,c1 is_collinear by A4, Th1; a1,c3,a2 is_collinear by A2, Th1; then a1,c1,a2 is_collinear by A5, A12, Th2; then A13: a2,c1,a1 is_collinear by Th1; a2,c1,a3 is_collinear by A3, Th1; then a2,a1,a3 is_collinear by A7, A13, Th2; hence contradiction by A1, Th1; ::_thesis: verum end; hence ( a1 <> x & a3 <> x ) by A9; ::_thesis: verum end; theorem Th10: :: HESSENBE:10 for PCPP being CollProjectiveSpace for a, b, c, d, e being Element of PCPP st not a,b,c is_collinear & a,b,d is_collinear & c,e,d is_collinear & e <> c & d <> a holds not e,a,c is_collinear proof let PCPP be CollProjectiveSpace; ::_thesis: for a, b, c, d, e being Element of PCPP st not a,b,c is_collinear & a,b,d is_collinear & c,e,d is_collinear & e <> c & d <> a holds not e,a,c is_collinear let a, b, c, d, e be Element of PCPP; ::_thesis: ( not a,b,c is_collinear & a,b,d is_collinear & c,e,d is_collinear & e <> c & d <> a implies not e,a,c is_collinear ) assume that A1: not a,b,c is_collinear and A2: a,b,d is_collinear and A3: ( c,e,d is_collinear & e <> c ) and A4: d <> a ; ::_thesis: not e,a,c is_collinear assume e,a,c is_collinear ; ::_thesis: contradiction then c,e,a is_collinear by Th1; then c,a,d is_collinear by A3, Th2; then A5: a,d,c is_collinear by Th1; a,d,b is_collinear by A2, Th1; hence contradiction by A1, A4, A5, Th2; ::_thesis: verum end; theorem Th11: :: HESSENBE:11 for PCPP being CollProjectiveSpace for p1, p2, q1, q2, q3 being Element of PCPP st not p1,p2,q1 is_collinear & p1,p2,q2 is_collinear & q1,q2,q3 is_collinear & q2 <> q3 holds not p2,p1,q3 is_collinear proof let PCPP be CollProjectiveSpace; ::_thesis: for p1, p2, q1, q2, q3 being Element of PCPP st not p1,p2,q1 is_collinear & p1,p2,q2 is_collinear & q1,q2,q3 is_collinear & q2 <> q3 holds not p2,p1,q3 is_collinear let p1, p2, q1, q2, q3 be Element of PCPP; ::_thesis: ( not p1,p2,q1 is_collinear & p1,p2,q2 is_collinear & q1,q2,q3 is_collinear & q2 <> q3 implies not p2,p1,q3 is_collinear ) assume that A1: not p1,p2,q1 is_collinear and A2: p1,p2,q2 is_collinear and A3: q1,q2,q3 is_collinear and A4: q2 <> q3 ; ::_thesis: not p2,p1,q3 is_collinear A5: p1 <> p2 by A1, ANPROJ_2:def_7; assume A6: p2,p1,q3 is_collinear ; ::_thesis: contradiction then p1,p2,q3 is_collinear by Th1; then p1,q2,q3 is_collinear by A2, A5, Th2; then A7: q2,q3,p1 is_collinear by Th1; p2,p1,q2 is_collinear by A2, Th1; then p2,q2,q3 is_collinear by A6, A5, Th2; then A8: q2,q3,p2 is_collinear by Th1; q2,q3,q1 is_collinear by A3, Th1; hence contradiction by A1, A4, A7, A8, ANPROJ_2:def_8; ::_thesis: verum end; theorem :: HESSENBE:12 for PCPP being CollProjectiveSpace for p1, p2, q1, p3, q2 being Element of PCPP st not p1,p2,q1 is_collinear & p1,p2,p3 is_collinear & q1,q2,p3 is_collinear & p3 <> q2 & p2 <> p3 holds not p3,p2,q2 is_collinear proof let PCPP be CollProjectiveSpace; ::_thesis: for p1, p2, q1, p3, q2 being Element of PCPP st not p1,p2,q1 is_collinear & p1,p2,p3 is_collinear & q1,q2,p3 is_collinear & p3 <> q2 & p2 <> p3 holds not p3,p2,q2 is_collinear let p1, p2, q1, p3, q2 be Element of PCPP; ::_thesis: ( not p1,p2,q1 is_collinear & p1,p2,p3 is_collinear & q1,q2,p3 is_collinear & p3 <> q2 & p2 <> p3 implies not p3,p2,q2 is_collinear ) assume that A1: not p1,p2,q1 is_collinear and A2: p1,p2,p3 is_collinear and A3: q1,q2,p3 is_collinear and A4: p3 <> q2 and A5: p2 <> p3 ; ::_thesis: not p3,p2,q2 is_collinear assume A6: p3,p2,q2 is_collinear ; ::_thesis: contradiction p3,p2,p1 is_collinear by A2, Th1; then A7: p3,q2,p1 is_collinear by A5, A6, Th2; A8: p3,q2,q1 is_collinear by A3, Th1; p3,q2,p2 is_collinear by A6, Th1; hence contradiction by A1, A4, A7, A8, ANPROJ_2:def_8; ::_thesis: verum end; theorem Th13: :: HESSENBE:13 for PCPP being CollProjectiveSpace for p1, p2, q1, p3, q2 being Element of PCPP st not p1,p2,q1 is_collinear & p1,p2,p3 is_collinear & q1,q2,p1 is_collinear & p1 <> p3 & p1 <> q2 holds not p3,p1,q2 is_collinear proof let PCPP be CollProjectiveSpace; ::_thesis: for p1, p2, q1, p3, q2 being Element of PCPP st not p1,p2,q1 is_collinear & p1,p2,p3 is_collinear & q1,q2,p1 is_collinear & p1 <> p3 & p1 <> q2 holds not p3,p1,q2 is_collinear let p1, p2, q1, p3, q2 be Element of PCPP; ::_thesis: ( not p1,p2,q1 is_collinear & p1,p2,p3 is_collinear & q1,q2,p1 is_collinear & p1 <> p3 & p1 <> q2 implies not p3,p1,q2 is_collinear ) assume that A1: not p1,p2,q1 is_collinear and A2: p1,p2,p3 is_collinear and A3: q1,q2,p1 is_collinear and A4: p1 <> p3 and A5: p1 <> q2 ; ::_thesis: not p3,p1,q2 is_collinear A6: p1,q2,q1 is_collinear by A3, Th1; assume p3,p1,q2 is_collinear ; ::_thesis: contradiction then A7: p1,p3,q2 is_collinear by Th1; p1,p3,p2 is_collinear by A2, Th1; then p1,q2,p2 is_collinear by A4, A7, Th2; hence contradiction by A1, A5, A6, Th2; ::_thesis: verum end; theorem Th14: :: HESSENBE:14 for PCPP being CollProjectiveSpace for a1, a2, b1, b2, x, y being Element of PCPP st a1 <> a2 & b1 <> b2 & b1,b2,x is_collinear & b1,b2,y is_collinear & a1,a2,x is_collinear & a1,a2,y is_collinear & not a1,a2,b1 is_collinear holds x = y proof let PCPP be CollProjectiveSpace; ::_thesis: for a1, a2, b1, b2, x, y being Element of PCPP st a1 <> a2 & b1 <> b2 & b1,b2,x is_collinear & b1,b2,y is_collinear & a1,a2,x is_collinear & a1,a2,y is_collinear & not a1,a2,b1 is_collinear holds x = y let a1, a2, b1, b2, x, y be Element of PCPP; ::_thesis: ( a1 <> a2 & b1 <> b2 & b1,b2,x is_collinear & b1,b2,y is_collinear & a1,a2,x is_collinear & a1,a2,y is_collinear & not a1,a2,b1 is_collinear implies x = y ) assume that A1: a1 <> a2 and A2: ( b1 <> b2 & b1,b2,x is_collinear & b1,b2,y is_collinear ) and A3: ( a1,a2,x is_collinear & a1,a2,y is_collinear ) and A4: not a1,a2,b1 is_collinear ; ::_thesis: x = y a1,a2,a2 is_collinear by ANPROJ_2:def_7; then A5: x,y,a2 is_collinear by A1, A3, ANPROJ_2:def_8; b1,b2,b1 is_collinear by ANPROJ_2:def_7; then A6: x,y,b1 is_collinear by A2, ANPROJ_2:def_8; assume A7: not x = y ; ::_thesis: contradiction a1,a2,a1 is_collinear by ANPROJ_2:def_7; then x,y,a1 is_collinear by A1, A3, ANPROJ_2:def_8; hence contradiction by A4, A7, A6, A5, ANPROJ_2:def_8; ::_thesis: verum end; theorem Th15: :: HESSENBE:15 for PCPP being CollProjectiveSpace 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 proof 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, Th6; then not o,a2,b1 is_collinear by Th1; then not o,b2,b1 is_collinear by A2, A4, Th6; hence not o,b1,b2 is_collinear by Th1; ::_thesis: verum end; theorem Th16: :: HESSENBE:16 for PCPP being Pappian CollProjectivePlane for p2, p3, p1, q2, q3, q1, r3, r2, r1 being Element of PCPP st p2 <> p3 & p1 <> p3 & q2 <> q3 & q1 <> q2 & q1 <> q3 & not p1,p2,q1 is_collinear & p1,p2,p3 is_collinear & q1,q2,q3 is_collinear & p1,q2,r3 is_collinear & q1,p2,r3 is_collinear & p1,q3,r2 is_collinear & p3,q1,r2 is_collinear & p2,q3,r1 is_collinear & p3,q2,r1 is_collinear holds r1,r2,r3 is_collinear proof let PCPP be Pappian CollProjectivePlane; ::_thesis: for p2, p3, p1, q2, q3, q1, r3, r2, r1 being Element of PCPP st p2 <> p3 & p1 <> p3 & q2 <> q3 & q1 <> q2 & q1 <> q3 & not p1,p2,q1 is_collinear & p1,p2,p3 is_collinear & q1,q2,q3 is_collinear & p1,q2,r3 is_collinear & q1,p2,r3 is_collinear & p1,q3,r2 is_collinear & p3,q1,r2 is_collinear & p2,q3,r1 is_collinear & p3,q2,r1 is_collinear holds r1,r2,r3 is_collinear let p2, p3, p1, q2, q3, q1, r3, r2, r1 be Element of PCPP; ::_thesis: ( p2 <> p3 & p1 <> p3 & q2 <> q3 & q1 <> q2 & q1 <> q3 & not p1,p2,q1 is_collinear & p1,p2,p3 is_collinear & q1,q2,q3 is_collinear & p1,q2,r3 is_collinear & q1,p2,r3 is_collinear & p1,q3,r2 is_collinear & p3,q1,r2 is_collinear & p2,q3,r1 is_collinear & p3,q2,r1 is_collinear implies r1,r2,r3 is_collinear ) assume that A1: p2 <> p3 and A2: p1 <> p3 and A3: q2 <> q3 and A4: q1 <> q2 and A5: q1 <> q3 and A6: not p1,p2,q1 is_collinear and A7: p1,p2,p3 is_collinear and A8: q1,q2,q3 is_collinear and A9: p1,q2,r3 is_collinear and A10: q1,p2,r3 is_collinear and A11: p1,q3,r2 is_collinear and A12: p3,q1,r2 is_collinear and A13: p2,q3,r1 is_collinear and A14: p3,q2,r1 is_collinear ; ::_thesis: r1,r2,r3 is_collinear A15: p1 <> p2 by A6, ANPROJ_2:def_7; A16: now__::_thesis:_(_not_p1,p2,q2_is_collinear_implies_r1,r2,r3_is_collinear_) assume A17: not p1,p2,q2 is_collinear ; ::_thesis: r1,r2,r3 is_collinear A18: now__::_thesis:_(_not_p1,p2,q3_is_collinear_implies_r1,r2,r3_is_collinear_) assume A19: not p1,p2,q3 is_collinear ; ::_thesis: r1,r2,r3 is_collinear A20: now__::_thesis:_(_(_q1,q2,p1_is_collinear_or_q1,q2,p2_is_collinear_or_q1,q2,p3_is_collinear_)_implies_r1,r2,r3_is_collinear_) A21: now__::_thesis:_(_q1,q2,p2_is_collinear_implies_r1,r2,r3_is_collinear_) ( not p2,p1,q2 is_collinear & p2,p1,p3 is_collinear ) by A7, A17, Th1; then not p2,p3,q2 is_collinear by A1, Th6; then A22: not q2,p2,p3 is_collinear by Th1; assume A23: q1,q2,p2 is_collinear ; ::_thesis: r1,r2,r3 is_collinear then A24: p2,q1,q2 is_collinear by Th1; ( p2 <> q1 & p2,q1,r3 is_collinear ) by A6, A10, Th1, ANPROJ_2:def_7; then p2,r3,q2 is_collinear by A24, Th2; then A25: q2,p2,r3 is_collinear by Th1; ( q2,p1,r3 is_collinear & not q2,p1,p2 is_collinear ) by A9, A17, Th1; then A26: q2 = r3 by A25, Th7; A27: q2,q1,q3 is_collinear by A8, Th1; q2,q1,p2 is_collinear by A23, Th1; then q2,p2,q3 is_collinear by A4, A27, Th2; then A28: p2,q3,q2 is_collinear by Th1; p2 <> q3 by A19, ANPROJ_2:def_7; then p2,r1,q2 is_collinear by A13, A28, Th2; then A29: q2,p2,r1 is_collinear by Th1; q2,p3,r1 is_collinear by A14, Th1; then q2 = r1 by A29, A22, Th7; hence r1,r2,r3 is_collinear by A26, ANPROJ_2:def_7; ::_thesis: verum end; A30: now__::_thesis:_(_q1,q2,p3_is_collinear_implies_r1,r2,r3_is_collinear_) ( not p2,p1,q3 is_collinear & p2,p1,p3 is_collinear ) by A7, A19, Th1; then not p2,p3,q3 is_collinear by A1, Th6; then A31: not q3,p2,p3 is_collinear by Th1; assume A32: q1,q2,p3 is_collinear ; ::_thesis: r1,r2,r3 is_collinear then A33: q2,q1,p3 is_collinear by Th1; q2,q1,q3 is_collinear by A8, Th1; then q2,q3,p3 is_collinear by A4, A33, Th2; then p3,q2,q3 is_collinear by Th1; then p3,r1,q3 is_collinear by A7, A14, A17, Th2; then A34: q3,p3,r1 is_collinear by Th1; not p1,p3,q3 is_collinear by A2, A7, A19, Th6; then A35: not q3,p1,p3 is_collinear by Th1; q1,q3,p3 is_collinear by A4, A8, A32, Th2; then p3,q1,q3 is_collinear by Th1; then p3,r2,q3 is_collinear by A6, A7, A12, Th2; then A36: q3,p3,r2 is_collinear by Th1; q3,p2,r1 is_collinear by A13, Th1; then A37: q3 = r1 by A34, A31, Th7; q3,p1,r2 is_collinear by A11, Th1; then q3 = r2 by A36, A35, Th7; hence r1,r2,r3 is_collinear by A37, ANPROJ_2:def_7; ::_thesis: verum end; A38: now__::_thesis:_(_q1,q2,p1_is_collinear_implies_r1,r2,r3_is_collinear_) not p1,p3,q1 is_collinear by A2, A6, A7, Th6; then A39: not q1,p1,p3 is_collinear by Th1; assume A40: q1,q2,p1 is_collinear ; ::_thesis: r1,r2,r3 is_collinear then q1,p1,q3 is_collinear by A4, A8, Th2; then A41: p1,q3,q1 is_collinear by Th1; p1 <> q3 by A19, ANPROJ_2:def_7; then p1,r2,q1 is_collinear by A11, A41, Th2; then A42: q1,p1,r2 is_collinear by Th1; A43: p1 <> q2 by A17, ANPROJ_2:def_7; p1,q2,q1 is_collinear by A40, Th1; then p1,r3,q1 is_collinear by A9, A43, Th2; then A44: q1,p1,r3 is_collinear by Th1; not q1,p2,p1 is_collinear by A6, Th1; then A45: q1 = r3 by A10, A44, Th7; q1,p3,r2 is_collinear by A12, Th1; then q1 = r2 by A42, A39, Th7; hence r1,r2,r3 is_collinear by A45, ANPROJ_2:def_7; ::_thesis: verum end; assume ( q1,q2,p1 is_collinear or q1,q2,p2 is_collinear or q1,q2,p3 is_collinear ) ; ::_thesis: r1,r2,r3 is_collinear hence r1,r2,r3 is_collinear by A38, A21, A30; ::_thesis: verum end; now__::_thesis:_(_not_q1,q2,p1_is_collinear_&_not_q1,q2,p2_is_collinear_&_not_q1,q2,p3_is_collinear_implies_r1,r2,r3_is_collinear_) assume that A46: not q1,q2,p1 is_collinear and A47: ( not q1,q2,p2 is_collinear & not q1,q2,p3 is_collinear ) ; ::_thesis: r1,r2,r3 is_collinear consider o being Element of PCPP such that A48: p1,p2,o is_collinear and A49: q1,q2,o is_collinear by ANPROJ_2:def_14; not p1,o,q1 is_collinear by A6, A46, A48, A49, Th6; then A50: not o,p1,q1 is_collinear by Th1; q1,q3,o is_collinear by A4, A8, A49, Th2; then A51: o,q1,q3 is_collinear by Th1; p1,p3,o is_collinear by A7, A15, A48, Th2; then A52: o,p1,p3 is_collinear by Th1; ( o,p1,p2 is_collinear & o,q1,q2 is_collinear ) by A48, A49, Th1; hence r1,r2,r3 is_collinear by A1, A2, A3, A4, A5, A9, A10, A11, A12, A13, A14, A15, A17, A19, A47, A48, A49, A52, A51, A50, ANPROJ_2:def_13; ::_thesis: verum end; hence r1,r2,r3 is_collinear by A20; ::_thesis: verum end; now__::_thesis:_(_p1,p2,q3_is_collinear_implies_r1,r2,r3_is_collinear_) assume A53: p1,p2,q3 is_collinear ; ::_thesis: r1,r2,r3 is_collinear A54: now__::_thesis:_(_p2_<>_q3_&_p1_<>_q3_implies_r1,r2,r3_is_collinear_) assume that A55: p2 <> q3 and A56: p1 <> q3 ; ::_thesis: r1,r2,r3 is_collinear p1,q3,p2 is_collinear by A53, Th1; then p1,p2,r2 is_collinear by A11, A56, Th2; then p1,r2,p3 is_collinear by A7, A15, Th2; then A57: p3,p1,r2 is_collinear by Th1; not p1,p3,q1 is_collinear by A2, A6, A7, Th6; then not p3,q1,p1 is_collinear by Th1; then A58: p3 = r2 by A12, A57, Th7; A59: p2,p1,p3 is_collinear by A7, Th1; p2,q3,p1 is_collinear by A53, Th1; then p2,p1,r1 is_collinear by A13, A55, Th2; then p2,r1,p3 is_collinear by A15, A59, Th2; then A60: p3,p2,r1 is_collinear by Th1; ( not p2,p1,q2 is_collinear & p2,p1,p3 is_collinear ) by A7, A17, Th1; then not p2,p3,q2 is_collinear by A1, Th6; then not p3,q2,p2 is_collinear by Th1; then p3 = r1 by A14, A60, Th7; hence r1,r2,r3 is_collinear by A58, ANPROJ_2:def_7; ::_thesis: verum end; A61: now__::_thesis:_(_p2_=_q3_implies_r1,r2,r3_is_collinear_) not p1,p3,q1 is_collinear by A2, A6, A7, Th6; then A62: not p3,p1,q1 is_collinear by Th1; A63: not p2,q1,p1 is_collinear by A6, Th1; A64: p2,q1,r3 is_collinear by A10, Th1; assume A65: p2 = q3 ; ::_thesis: r1,r2,r3 is_collinear then p2,q1,q2 is_collinear by A8, Th1; then p2,q2,r3 is_collinear by A5, A65, A64, Th2; then A66: q2,p2,r3 is_collinear by Th1; p2,q1,q2 is_collinear by A8, A65, Th1; then not p2,q2,p1 is_collinear by A3, A65, A63, Th6; then A67: not q2,p1,p2 is_collinear by Th1; p1,p3,r2 is_collinear by A7, A11, A15, A65, Th2; then p3,p1,r2 is_collinear by Th1; then A68: p3 = r2 by A12, A62, Th7; q2,p1,r3 is_collinear by A9, Th1; then q2 = r3 by A66, A67, Th7; hence r1,r2,r3 is_collinear by A14, A68, Th1; ::_thesis: verum end; now__::_thesis:_(_p1_=_q3_implies_r1,r2,r3_is_collinear_) assume A69: p1 = q3 ; ::_thesis: r1,r2,r3 is_collinear then p1,p2,r1 is_collinear by A13, Th1; then p1,p3,r1 is_collinear by A7, A15, Th2; then A70: p3,p1,r1 is_collinear by Th1; p1,q2,q1 is_collinear by A8, A69, Th1; then p1,q1,r3 is_collinear by A3, A9, A69, Th2; then A71: q1,p1,r3 is_collinear by Th1; not p3,p1,q2 is_collinear by A2, A3, A6, A7, A8, A69, Th13; then A72: p3 = r1 by A14, A70, Th7; not q1,p1,p2 is_collinear by A6, Th1; then q1 = r3 by A10, A71, Th7; hence r1,r2,r3 is_collinear by A12, A72, Th1; ::_thesis: verum end; hence r1,r2,r3 is_collinear by A61, A54; ::_thesis: verum end; hence r1,r2,r3 is_collinear by A18; ::_thesis: verum end; now__::_thesis:_(_p1,p2,q2_is_collinear_implies_r1,r2,r3_is_collinear_) A73: now__::_thesis:_(_p1_=_q2_implies_r1,r2,r3_is_collinear_) not p1,p3,q1 is_collinear by A2, A6, A7, Th6; then A74: not q1,p1,p3 is_collinear by Th1; A75: not p1,q1,p2 is_collinear by A6, Th1; assume A76: p1 = q2 ; ::_thesis: r1,r2,r3 is_collinear then p1,q3,q1 is_collinear by A8, Th1; then p1,q1,r2 is_collinear by A3, A11, A76, Th2; then A77: q1,p1,r2 is_collinear by Th1; A78: p1,p3,p2 is_collinear by A7, Th1; p1,p3,r1 is_collinear by A14, A76, Th1; then p1,p2,r1 is_collinear by A2, A78, Th2; then A79: p2,p1,r1 is_collinear by Th1; q1,p3,r2 is_collinear by A12, Th1; then A80: q1 = r2 by A77, A74, Th7; p1,q1,q3 is_collinear by A8, A76, Th1; then not p1,q3,p2 is_collinear by A3, A76, A75, Th6; then not p2,p1,q3 is_collinear by Th1; then r1 = p2 by A13, A79, Th7; hence r1,r2,r3 is_collinear by A10, A80, Th1; ::_thesis: verum end; assume A81: p1,p2,q2 is_collinear ; ::_thesis: r1,r2,r3 is_collinear A82: now__::_thesis:_(_p1_<>_q2_&_p3_<>_q2_implies_r1,r2,r3_is_collinear_) assume that A83: p1 <> q2 and A84: p3 <> q2 ; ::_thesis: r1,r2,r3 is_collinear p1,q2,p2 is_collinear by A81, Th1; then p1,p2,r3 is_collinear by A9, A83, Th2; then A85: p2,p1,r3 is_collinear by Th1; p1,q2,p3 is_collinear by A7, A15, A81, Th2; then p3,q2,p1 is_collinear by Th1; then p3,p1,r1 is_collinear by A14, A84, Th2; then A86: p1,p3,r1 is_collinear by Th1; p1,p3,p2 is_collinear by A7, Th1; then p1,p2,r1 is_collinear by A2, A86, Th2; then A87: p2,p1,r1 is_collinear by Th1; not p2,p1,q3 is_collinear by A3, A6, A8, A81, Th11; then A88: p2 = r1 by A13, A87, Th7; ( not p2,p1,q1 is_collinear & p2,q1,r3 is_collinear ) by A6, A10, Th1; then p2 = r3 by A85, Th7; hence r1,r2,r3 is_collinear by A88, ANPROJ_2:def_7; ::_thesis: verum end; now__::_thesis:_(_p3_=_q2_implies_r1,r2,r3_is_collinear_) assume A89: p3 = q2 ; ::_thesis: r1,r2,r3 is_collinear then q1,q3,p3 is_collinear by A8, Th1; then A90: not q3,p1,q1 is_collinear by A2, A5, A6, A7, Th10; p1,p3,p2 is_collinear by A7, Th1; then p1,p2,r3 is_collinear by A2, A9, A89, Th2; then A91: p2,p1,r3 is_collinear by Th1; ( not p2,p1,q1 is_collinear & p2,q1,r3 is_collinear ) by A6, A10, Th1; then A92: p2 = r3 by A91, Th7; q1,q2,r2 is_collinear by A12, A89, Th1; then q1,q3,r2 is_collinear by A4, A8, Th2; then A93: q3,q1,r2 is_collinear by Th1; q3,p1,r2 is_collinear by A11, Th1; then r3,r2,r1 is_collinear by A13, A92, A90, A93, Th7; hence r1,r2,r3 is_collinear by Th1; ::_thesis: verum end; hence r1,r2,r3 is_collinear by A73, A82; ::_thesis: verum end; hence r1,r2,r3 is_collinear by A16; ::_thesis: verum end; Lm1: for PCPP being Pappian CollProjectivePlane for o, b1, b2, a1, a2, a3, c3, c1, b3, c2 being Element of PCPP st o <> b1 & o <> b2 & 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 & ( a1,a2,a3 is_collinear or b1,b2,b3 is_collinear ) holds c1,c2,c3 is_collinear proof let PCPP be Pappian CollProjectivePlane; ::_thesis: for o, b1, b2, a1, a2, a3, c3, c1, b3, c2 being Element of PCPP st o <> b1 & o <> b2 & 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 & ( a1,a2,a3 is_collinear or b1,b2,b3 is_collinear ) holds c1,c2,c3 is_collinear let o, b1, b2, a1, a2, a3, c3, c1, b3, c2 be Element of PCPP; ::_thesis: ( o <> b1 & o <> b2 & 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 & ( a1,a2,a3 is_collinear or b1,b2,b3 is_collinear ) implies c1,c2,c3 is_collinear ) assume that A1: o <> b1 and A2: o <> b2 and A3: not o,a1,a2 is_collinear and A4: not o,a1,a3 is_collinear and A5: not o,a2,a3 is_collinear and A6: a1,a2,c3 is_collinear and A7: b1,b2,c3 is_collinear and A8: a2,a3,c1 is_collinear and A9: b2,b3,c1 is_collinear and A10: a1,a3,c2 is_collinear and A11: b1,b3,c2 is_collinear and A12: o,a1,b1 is_collinear and A13: o,a2,b2 is_collinear and A14: o,a3,b3 is_collinear and A15: ( a1,a2,a3 is_collinear or b1,b2,b3 is_collinear ) ; ::_thesis: c1,c2,c3 is_collinear A16: a1 <> a3 by A4, ANPROJ_2:def_7; A17: a2 <> a3 by A5, ANPROJ_2:def_7; A18: a1 <> a2 by A3, ANPROJ_2:def_7; A19: now__::_thesis:_(_a1,a2,a3_is_collinear_implies_c1,c2,c3_is_collinear_) assume A20: a1,a2,a3 is_collinear ; ::_thesis: c1,c2,c3 is_collinear then a2,a3,a1 is_collinear by Th1; then a2,a1,c1 is_collinear by A8, A17, Th2; then A21: a1,a2,c1 is_collinear by Th1; a1,a3,a2 is_collinear by A20, Th1; then a1,a2,c2 is_collinear by A10, A16, Th2; hence c1,c2,c3 is_collinear by A6, A18, A21, ANPROJ_2:def_8; ::_thesis: verum end; A22: b2 <> b3 by A2, A5, A13, A14, Th7; A23: b1 <> b3 by A1, A4, A12, A14, Th7; A24: b1 <> b2 by A1, A3, A12, A13, Th7; now__::_thesis:_(_b1,b2,b3_is_collinear_implies_c1,c2,c3_is_collinear_) assume A25: b1,b2,b3 is_collinear ; ::_thesis: c1,c2,c3 is_collinear then b2,b3,b1 is_collinear by Th1; then b2,b1,c1 is_collinear by A9, A22, Th2; then A26: b1,b2,c1 is_collinear by Th1; b1,b3,b2 is_collinear by A25, Th1; then b1,b2,c2 is_collinear by A11, A23, Th2; hence c1,c2,c3 is_collinear by A7, A24, A26, ANPROJ_2:def_8; ::_thesis: verum end; hence c1,c2,c3 is_collinear by A15, A19; ::_thesis: verum end; Lm2: for PCPP being Pappian CollProjectivePlane for o, b1, a1, b2, a2, b3, a3, c1, c3, c2, x 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 & not o,c1,c3 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 & o,a2,x is_collinear & a1,a3,x is_collinear & not c1,c3,x is_collinear holds c1,c2,c3 is_collinear proof let PCPP be Pappian CollProjectivePlane; ::_thesis: for o, b1, a1, b2, a2, b3, a3, c1, c3, c2, x 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 & not o,c1,c3 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 & o,a2,x is_collinear & a1,a3,x is_collinear & not c1,c3,x is_collinear holds c1,c2,c3 is_collinear let o, b1, a1, b2, a2, b3, a3, c1, c3, c2, x 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 & not o,c1,c3 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 & o,a2,x is_collinear & a1,a3,x is_collinear & not c1,c3,x is_collinear implies c1,c2,c3 is_collinear ) assume that A1: o <> b1 and A2: a1 <> b1 and A3: o <> b2 and A4: a2 <> b2 and A5: o <> b3 and A6: a3 <> b3 and A7: not o,a1,a2 is_collinear and A8: not o,a1,a3 is_collinear and A9: not o,a2,a3 is_collinear and A10: not o,c1,c3 is_collinear and A11: a1,a2,c3 is_collinear and A12: b1,b2,c3 is_collinear and A13: a2,a3,c1 is_collinear and A14: b2,b3,c1 is_collinear and A15: a1,a3,c2 is_collinear and A16: b1,b3,c2 is_collinear and A17: o,a1,b1 is_collinear and A18: o,a2,b2 is_collinear and A19: o,a3,b3 is_collinear and A20: o,a2,x is_collinear and A21: a1,a3,x is_collinear and A22: not c1,c3,x is_collinear ; ::_thesis: c1,c2,c3 is_collinear A23: o <> a1 by A7, ANPROJ_2:def_7; A24: b1 <> b3 by A1, A8, A17, A19, Th7; A25: a1 <> a2 by A7, ANPROJ_2:def_7; A26: o <> a2 by A7, ANPROJ_2:def_7; A27: o <> a3 by A8, ANPROJ_2:def_7; A28: a1 <> a3 by A8, ANPROJ_2:def_7; A29: a2 <> a3 by A9, ANPROJ_2:def_7; ( not a1,o,a3 is_collinear & a1,o,b1 is_collinear ) by A8, A17, Th1; then not a1,b1,a3 is_collinear by A2, Th6; then A30: not a1,a3,b1 is_collinear by Th1; A31: now__::_thesis:_(_not_a1,a2,a3_is_collinear_&_not_b1,b2,b3_is_collinear_implies_c1,c2,c3_is_collinear_) ( not o,a2,a1 is_collinear & b2,b1,c3 is_collinear ) by A7, A12, Th1; then A32: a1 <> c3 by A2, A3, A17, A18, Th8; not a1,a2,o is_collinear by A7, Th1; then not a1,c3,o is_collinear by A11, A32, Th6; then A33: not o,a1,c3 is_collinear by Th1; A34: c1 <> c3 by A10, ANPROJ_2:def_7; o <> x by A8, A21, Th1; then not o,x,a3 is_collinear by A9, A20, Th6; then A35: not x,a3,o is_collinear by Th1; A36: a1 <> a3 by A8, ANPROJ_2:def_7; ( not o,a2,a1 is_collinear & b2,b1,c3 is_collinear ) by A7, A12, Th1; then A37: a1 <> c3 by A2, A3, A17, A18, Th8; A38: a2,a1,c3 is_collinear by A11, Th1; A39: a2,a1,c3 is_collinear by A11, Th1; A40: a2 <> c3 by A1, A4, A7, A12, A17, A18, Th8; not o,b2,a3 is_collinear by A3, A9, A18, Th6; then A41: not a3,o,b2 is_collinear by Th1; A42: c1 <> c3 by A10, ANPROJ_2:def_7; A43: o,b1,a1 is_collinear by A17, Th1; A44: not a1,a3,o is_collinear by A8, Th1; ( not o,a3,a2 is_collinear & b3,b2,c1 is_collinear ) by A9, A14, Th1; then A45: a2 <> c1 by A4, A5, A18, A19, Th8; a3,b3,o is_collinear by A19, Th1; then not b2,o,b3 is_collinear by A3, A5, A9, A18, Th13; then A46: not o,b3,b2 is_collinear by Th1; A47: o <> a2 by A7, ANPROJ_2:def_7; assume that A48: not a1,a2,a3 is_collinear and A49: not b1,b2,b3 is_collinear ; ::_thesis: c1,c2,c3 is_collinear A50: b1 <> b3 by A49, ANPROJ_2:def_7; consider z being Element of PCPP such that A51: a1,a3,z is_collinear and A52: c1,c3,z is_collinear by ANPROJ_2:def_14; consider p being Element of PCPP such that A53: o,z,p is_collinear and A54: a2,a3,p is_collinear by ANPROJ_2:def_14; A55: o <> p by A9, A54, Th1; A56: a3 <> c1 by A3, A6, A9, A14, A18, A19, Th8; then A57: a1 <> z by A11, A13, A48, A52, A40, A45, A37, Th9; A58: a3 <> z by A11, A13, A48, A52, A40, A45, A37, A56, Th9; A59: a3 <> p proof assume not a3 <> p ; ::_thesis: contradiction then A60: a3,o,z is_collinear by A53, Th1; ( a3,a1,z is_collinear & not a3,o,a1 is_collinear ) by A8, A51, Th1; hence contradiction by A58, A60, Th7; ::_thesis: verum end; A61: a3,a1,x is_collinear by A21, Th1; A62: o,b2,a2 is_collinear by A18, Th1; a1 <> z by A11, A13, A48, A52, A40, A45, A37, A56, Th9; then not a1,z,o is_collinear by A51, A44, Th6; then not o,z,a1 is_collinear by Th1; then not o,p,a1 is_collinear by A53, A55, Th6; then A63: not o,a1,p is_collinear by Th1; A64: a3,z,a1 is_collinear by A51, Th1; A65: p,a2,a3 is_collinear by A54, Th1; consider q being Element of PCPP such that A66: o,a1,q is_collinear and A67: p,c3,q is_collinear by ANPROJ_2:def_14; consider r being Element of PCPP such that A68: p,b2,r is_collinear and A69: q,a3,r is_collinear by ANPROJ_2:def_14; A70: a3,q,r is_collinear by A69, Th1; ( o,b3,a3 is_collinear & a3,a2,c1 is_collinear ) by A13, A19, Th1; then A71: b2 <> c1 by A4, A27, A62, A46, Th8; A72: a2 <> c3 by A1, A4, A7, A12, A17, A18, Th8; not a1,a3,o is_collinear by A8, Th1; then not a1,z,o is_collinear by A51, A57, Th6; then not o,z,a1 is_collinear by Th1; then not o,p,a1 is_collinear by A53, A55, Th6; then A73: b1 <> p by A17, Th1; consider a being Element of PCPP such that A74: c1,c3,a is_collinear and A75: o,a2,a is_collinear by ANPROJ_2:def_14; A76: c3,c1,a is_collinear by A74, Th1; A77: a,o,a2 is_collinear by A75, Th1; A78: o <> a by A10, A74, Th1; A79: c1 <> c3 by A10, ANPROJ_2:def_7; A80: a2 <> a proof A81: c3,a2,a1 is_collinear by A11, Th1; assume A82: not a2 <> a ; ::_thesis: contradiction then c3,a2,c1 is_collinear by A74, Th1; then c3,c1,a1 is_collinear by A40, A81, Th2; then A83: c1,c3,a1 is_collinear by Th1; A84: c1,a2,a3 is_collinear by A13, Th1; c1,a2,c3 is_collinear by A74, A82, Th1; then c1,c3,a3 is_collinear by A45, A84, Th2; hence contradiction by A48, A74, A79, A82, A83, ANPROJ_2:def_8; ::_thesis: verum end; assume A85: not c1,c2,c3 is_collinear ; ::_thesis: contradiction c3,c1,z is_collinear by A52, Th1; then c3,a,z is_collinear by A76, A42, Th2; then A86: a,z,c3 is_collinear by Th1; A87: o,x,a is_collinear by A20, A26, A75, Th2; consider q9 being Element of PCPP such that A88: ( o,a1,q9 is_collinear & a,a3,q9 is_collinear ) by ANPROJ_2:def_14; a3,a2,p is_collinear by A54, Th1; then c3,q9,p is_collinear by A9, A53, A75, A88, A80, A78, A36, A57, A58, A64, A39, A86, Th16; then A89: p,c3,q9 is_collinear by Th1; not a2,a1,a3 is_collinear by A48, Th1; then not a2,c3,a3 is_collinear by A72, A38, Th6; then p <> c3 by A54, Th1; then A90: a,a3,q is_collinear by A23, A66, A67, A88, A89, A63, Th14; then a3,q,a is_collinear by Th1; then A91: a3,r,a is_collinear by A8, A66, A70, Th2; ( not o,a3,a2 is_collinear & b3,b2,c1 is_collinear ) by A9, A14, Th1; then A92: a2 <> c1 by A4, A5, A18, A19, Th8; A93: a <> a2 proof A94: c3,a2,a1 is_collinear by A11, Th1; assume A95: not a <> a2 ; ::_thesis: contradiction then c3,a2,c1 is_collinear by A74, Th1; then c3,c1,a1 is_collinear by A72, A94, Th2; then A96: c1,c3,a1 is_collinear by Th1; A97: c1,a2,a3 is_collinear by A13, Th1; c1,a2,c3 is_collinear by A74, A95, Th1; then c1,c3,a3 is_collinear by A92, A97, Th2; hence contradiction by A48, A74, A34, A95, A96, ANPROJ_2:def_8; ::_thesis: verum end; consider z99 being Element of PCPP such that A98: ( b3,r,z99 is_collinear & o,p,z99 is_collinear ) by ANPROJ_2:def_14; a2,b2,o is_collinear by A18, Th1; then A99: not b1,o,b2 is_collinear by A1, A3, A7, A17, Th13; then not o,b1,b2 is_collinear by Th1; then A100: b2 <> c3 by A4, A11, A23, A43, A62, Th8; A101: a <> b2 proof A102: c3,b2,b1 is_collinear by A12, Th1; assume A103: not a <> b2 ; ::_thesis: contradiction then c3,b2,c1 is_collinear by A74, Th1; then c3,c1,b1 is_collinear by A100, A102, Th2; then A104: c1,c3,b1 is_collinear by Th1; A105: c1,b2,b3 is_collinear by A14, Th1; c1,b2,c3 is_collinear by A74, A103, Th1; then c1,c3,b3 is_collinear by A71, A105, Th2; hence contradiction by A49, A74, A34, A103, A104, ANPROJ_2:def_8; ::_thesis: verum end; not a2,a3,o is_collinear by A9, Th1; then not a2,c1,o is_collinear by A13, A92, Th6; then A106: a <> c1 by A75, Th1; ( not a2,a1,o is_collinear & a2,a1,c3 is_collinear ) by A7, A11, Th1; then not a2,c3,o is_collinear by A72, Th6; then A107: a <> c3 by A75, Th1; o,a,b2 is_collinear by A18, A26, A75, Th2; then A108: a,o,b2 is_collinear by Th1; ( a2,o,b2 is_collinear & not a2,o,a3 is_collinear ) by A9, A18, Th1; then A109: not a2,b2,a3 is_collinear by A4, Th6; then A110: b2 <> p by A54, Th1; a3,a1,z is_collinear by A51, Th1; then a3,x,z is_collinear by A36, A61, Th2; then x,a3,z is_collinear by Th1; then not x,z,o is_collinear by A22, A52, A35, Th6; then not o,z,x is_collinear by Th1; then not o,p,x is_collinear by A53, A55, Th6; then not o,x,p is_collinear by Th1; then A111: not o,a,p is_collinear by A78, A87, Th6; then not a,o,p is_collinear by Th1; then not a,a2,p is_collinear by A93, A77, Th6; then not p,a2,a is_collinear by Th1; then A112: not p,a3,a is_collinear by A59, A65, Th6; then A113: p <> r by A91, Th1; o,a,b2 is_collinear by A18, A26, A75, Th2; then not o,b2,p is_collinear by A3, A111, Th6; then not p,b2,o is_collinear by Th1; then not p,r,o is_collinear by A68, A113, Th6; then A114: z <> r by A53, Th1; consider z9 being Element of PCPP such that A115: ( b1,r,z9 is_collinear & o,p,z9 is_collinear ) by ANPROJ_2:def_14; A116: not o,a,a3 is_collinear by A9, A75, A78, Th6; then not a,o,a3 is_collinear by Th1; then A117: not a,b2,a3 is_collinear by A101, A108, Th6; then A118: b2 <> r by A91, Th1; A119: now__::_thesis:_not_b1_<>_q o,b1,q is_collinear by A17, A23, A66, Th2; then A120: b1,o,q is_collinear by Th1; assume b1 <> q ; ::_thesis: contradiction then not b1,q,b2 is_collinear by A99, A120, Th6; then A121: not q,b1,b2 is_collinear by Th1; A122: ( b2,p,r is_collinear & q,p,c3 is_collinear ) by A67, A68, Th1; o,b1,q is_collinear by A17, A23, A66, Th2; then A123: q,b1,o is_collinear by Th1; A124: ( q <> o & b2 <> p ) by A54, A116, A109, A90, Th1; ( c3,c1,z is_collinear & c3,c1,a is_collinear ) by A52, A74, Th1; then c3,z,a is_collinear by A34, Th2; then A125: a,c3,z is_collinear by Th1; A126: ( not c1,c3,o is_collinear & o,p,z is_collinear ) by A10, A53, Th1; ( a3,a2,c1 is_collinear & a3,a2,p is_collinear ) by A13, A54, Th1; then A127: a3,p,c1 is_collinear by A29, Th2; o,a,b2 is_collinear by A18, A26, A75, Th2; then A128: b2,o,a is_collinear by Th1; q,a3,a is_collinear by A90, Th1; then A129: q,r,a is_collinear by A8, A66, A69, Th2; A130: ( b2 <> r & p <> r ) by A117, A91, A112, Th1; ( b2,b1,c3 is_collinear & o,b2,a is_collinear ) by A12, A18, A26, A75, Th1, Th2; then z9,a,c3 is_collinear by A1, A115, A124, A130, A121, A123, A122, A129, Th16; then A131: a,c3,z9 is_collinear by Th1; A132: b3,b2,c1 is_collinear by A14, Th1; ( a3,o,b3 is_collinear & b2,r,p is_collinear ) by A19, A68, Th1; then z99,c1,a is_collinear by A5, A6, A98, A110, A91, A118, A41, A113, A128, A127, A132, Th16; then A133: c1,a,z99 is_collinear by Th1; c1,a,c3 is_collinear by A74, Th1; then c1,c3,z99 is_collinear by A106, A133, Th2; then b3,r,z is_collinear by A52, A98, A34, A55, A126, Th14; then A134: z,r,b3 is_collinear by Th1; ( o,p,z is_collinear & not o,p,a is_collinear ) by A53, A111, Th1; then b1,r,z is_collinear by A115, A55, A107, A125, A131, Th14; then z,r,b1 is_collinear by Th1; then z,b1,b3 is_collinear by A114, A134, Th2; then b1,b3,z is_collinear by Th1; then c1,c3,c2 is_collinear by A15, A16, A28, A30, A50, A51, A52, Th14; hence contradiction by A85, Th1; ::_thesis: verum end; A135: not p,o,a is_collinear by A111, Th1; now__::_thesis:_not_b1_=_q ( a3,a2,c1 is_collinear & a3,a2,p is_collinear ) by A13, A54, Th1; then a3,c1,p is_collinear by A29, Th2; then A136: p,a3,c1 is_collinear by Th1; A137: b1,c3,b2 is_collinear by A12, Th1; ( not a1,o,a3 is_collinear & a1,o,b1 is_collinear ) by A8, A17, Th1; then not a1,b1,a3 is_collinear by A2, Th6; then A138: not a1,a3,b1 is_collinear by Th1; assume A139: b1 = q ; ::_thesis: contradiction then A140: b1,a3,a is_collinear by A90, Th1; c1,a,z is_collinear by A52, A74, A34, Th2; then A141: a,c1,z is_collinear by Th1; a2,b2,o is_collinear by A18, Th1; then not b1,o,b2 is_collinear by A1, A3, A7, A17, Th13; then A142: not b1,b2,o is_collinear by Th1; consider z9 being Element of PCPP such that A143: ( b1,b3,z9 is_collinear & p,o,z9 is_collinear ) by ANPROJ_2:def_14; b1,c3,p is_collinear by A67, A139, Th1; then A144: b1,b2,p is_collinear by A17, A33, A137, Th2; o,b2,a is_collinear by A18, A75, A47, Th2; then c1,z9,a is_collinear by A5, A6, A14, A19, A27, A73, A110, A143, A144, A142, A140, A136, Th16; then A145: a,c1,z9 is_collinear by Th1; p,o,z is_collinear by A53, Th1; then b1,b3,z is_collinear by A55, A106, A135, A143, A145, A141, Th14; then c1,c3,c2 is_collinear by A15, A16, A28, A50, A51, A52, A138, Th14; hence contradiction by A85, Th1; ::_thesis: verum end; hence contradiction by A119; ::_thesis: verum end; A146: b2 <> b3 by A3, A9, A18, A19, Th7; A147: b1 <> b2 by A1, A7, A17, A18, Th7; now__::_thesis:_(_(_a1,a2,a3_is_collinear_or_b1,b2,b3_is_collinear_)_implies_c1,c2,c3_is_collinear_) A148: now__::_thesis:_(_b1,b2,b3_is_collinear_implies_c1,c2,c3_is_collinear_) assume A149: b1,b2,b3 is_collinear ; ::_thesis: c1,c2,c3 is_collinear then b2,b3,b1 is_collinear by Th1; then b2,b1,c1 is_collinear by A14, A146, Th2; then A150: b1,b2,c1 is_collinear by Th1; b1,b3,b2 is_collinear by A149, Th1; then b1,b2,c2 is_collinear by A16, A24, Th2; hence c1,c2,c3 is_collinear by A12, A147, A150, ANPROJ_2:def_8; ::_thesis: verum end; A151: now__::_thesis:_(_a1,a2,a3_is_collinear_implies_c1,c2,c3_is_collinear_) assume A152: a1,a2,a3 is_collinear ; ::_thesis: c1,c2,c3 is_collinear then a2,a3,a1 is_collinear by Th1; then a2,a1,c1 is_collinear by A13, A29, Th2; then A153: a1,a2,c1 is_collinear by Th1; a1,a3,a2 is_collinear by A152, Th1; then a1,a2,c2 is_collinear by A15, A28, Th2; hence c1,c2,c3 is_collinear by A11, A25, A153, ANPROJ_2:def_8; ::_thesis: verum end; assume ( a1,a2,a3 is_collinear or b1,b2,b3 is_collinear ) ; ::_thesis: c1,c2,c3 is_collinear hence c1,c2,c3 is_collinear by A151, A148; ::_thesis: verum end; hence c1,c2,c3 is_collinear by A31; ::_thesis: verum end; Lm3: for PCPP being Pappian CollProjectivePlane for o, b1, a1, b2, a2, b3, a3, c1, c3, 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 & not o,c1,c3 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 proof let PCPP be Pappian CollProjectivePlane; ::_thesis: for o, b1, a1, b2, a2, b3, a3, c1, c3, 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 & not o,c1,c3 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, c1, c3, 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 & not o,c1,c3 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 and A2: a1 <> b1 and A3: o <> b2 and A4: a2 <> b2 and A5: o <> b3 and A6: a3 <> b3 and A7: not o,a1,a2 is_collinear and A8: not o,a1,a3 is_collinear and A9: not o,a2,a3 is_collinear and A10: not o,c1,c3 is_collinear and A11: ( a1,a2,c3 is_collinear & b1,b2,c3 is_collinear ) and A12: a2,a3,c1 is_collinear and A13: b2,b3,c1 is_collinear and A14: ( a1,a3,c2 is_collinear & b1,b3,c2 is_collinear ) and A15: o,a1,b1 is_collinear and A16: o,a2,b2 is_collinear and A17: o,a3,b3 is_collinear ; ::_thesis: c1,c2,c3 is_collinear A18: o <> a2 by A7, ANPROJ_2:def_7; A19: a1 <> a3 by A8, ANPROJ_2:def_7; A20: ( o <> a1 & o <> a3 ) by A8, ANPROJ_2:def_7; now__::_thesis:_(_not_a1,a2,a3_is_collinear_&_not_b1,b2,b3_is_collinear_&_not_c1,c2,c3_is_collinear_implies_c1,c2,c3_is_collinear_) assume that not a1,a2,a3 is_collinear and not b1,b2,b3 is_collinear ; ::_thesis: ( not c1,c2,c3 is_collinear implies c1,c2,c3 is_collinear ) consider x being Element of PCPP such that A21: a1,a3,x is_collinear and A22: o,a2,x is_collinear by ANPROJ_2:def_14; consider y being Element of PCPP such that A23: b1,b3,y is_collinear and A24: o,a2,y is_collinear by ANPROJ_2:def_14; assume A25: not c1,c2,c3 is_collinear ; ::_thesis: c1,c2,c3 is_collinear A26: now__::_thesis:_(_c1,c3,x_is_collinear_implies_not_c1,c3,y_is_collinear_) ( not o,a3,a2 is_collinear & b3,b2,c1 is_collinear ) by A9, A13, Th1; then A27: a2 <> c1 by A4, A5, A16, A17, Th8; not a2,a3,o is_collinear by A9, Th1; then not a2,c1,o is_collinear by A12, A27, Th6; then A28: not o,a2,c1 is_collinear by Th1; A29: b1 <> b3 by A1, A8, A15, A17, Th7; ( not a1,o,a3 is_collinear & a1,o,b1 is_collinear ) by A8, A15, Th1; then not a1,b1,a3 is_collinear by A2, Th6; then A30: not a1,a3,b1 is_collinear by Th1; assume that A31: c1,c3,x is_collinear and A32: c1,c3,y is_collinear ; ::_thesis: contradiction ( c1 <> c3 & o <> a2 ) by A7, A10, ANPROJ_2:def_7; then b1,b3,x is_collinear by A22, A23, A24, A31, A32, A28, Th14; then c1,c3,c2 is_collinear by A14, A19, A21, A31, A29, A30, Th14; hence contradiction by A25, Th1; ::_thesis: verum end; now__::_thesis:_(_(_not_c1,c3,x_is_collinear_or_not_c1,c3,y_is_collinear_)_implies_c1,c2,c3_is_collinear_) A33: now__::_thesis:_c1,c3,y_is_collinear A34: not o,b1,b3 is_collinear by A1, A5, A8, A15, A17, Th15; A35: ( o,b2,a2 is_collinear & o,b3,a3 is_collinear ) by A16, A17, Th1; A36: ( o,b2,y is_collinear & o,b1,a1 is_collinear ) by A15, A16, A18, A24, Th1, Th2; assume A37: not c1,c3,y is_collinear ; ::_thesis: contradiction ( not o,b1,b2 is_collinear & not o,b2,b3 is_collinear ) by A1, A3, A5, A7, A9, A15, A16, A17, Th15; hence contradiction by A2, A4, A6, A10, A11, A12, A13, A14, A18, A20, A23, A25, A37, A36, A35, A34, Lm2; ::_thesis: verum end; assume ( not c1,c3,x is_collinear or not c1,c3,y is_collinear ) ; ::_thesis: c1,c2,c3 is_collinear hence c1,c2,c3 is_collinear by A1, A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, A12, A13, A14, A15, A16, A17, A21, A22, A33, Lm2; ::_thesis: verum end; hence c1,c2,c3 is_collinear by A26; ::_thesis: verum end; hence c1,c2,c3 is_collinear by A1, A3, A7, A8, A9, A11, A12, A13, A14, A15, A16, A17, Lm1; ::_thesis: verum end; theorem Th17: :: HESSENBE:17 for PCPP being Pappian CollProjectivePlane 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 proof 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, Th1; A8: b3,b2,c1 is_collinear by A5, Th1; A9: ( not o,a3,a2 is_collinear & a3,a2,c1 is_collinear ) by A2, A4, Th1; now__::_thesis:_(_o,c1,c3_is_collinear_implies_c1,c2,c3_is_collinear_) assume o,c1,c3 is_collinear ; ::_thesis: c1,c2,c3 is_collinear then A10: c1,c3,o is_collinear by Th1; assume not c1,c2,c3 is_collinear ; ::_thesis: contradiction then A11: not c1,c3,c2 is_collinear by Th1; then not c1,o,c2 is_collinear by A7, A10, Th6; then not o,c1,c2 is_collinear by Th1; 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 end; registration clusterV38() V101() V102() proper Vebleian at_least_3rank Pappian -> Desarguesian for L13(); coherence for b1 being CollProjectiveSpace st b1 is Pappian holds b1 is Desarguesian proof let PCPP be CollProjectiveSpace; ::_thesis: ( PCPP is Pappian implies PCPP is Desarguesian ) assume A1: PCPP is Pappian ; ::_thesis: PCPP is Desarguesian A2: now__::_thesis:_(_(_for_p,_p1,_q,_q1_being_Element_of_PCPP_ex_r_being_Element_of_PCPP_st_ (_p,p1,r_is_collinear_&_q,q1,r_is_collinear_)_)_implies_PCPP_is_Desarguesian_) assume for p, p1, q, q1 being Element of PCPP ex r being Element of PCPP st ( p,p1,r is_collinear & q,q1,r is_collinear ) ; ::_thesis: PCPP is Desarguesian then PCPP is Pappian CollProjectivePlane by A1, ANPROJ_2:def_14; then for o, p1, p2, p3, q1, q2, q3, r1, r2, r3 being Element of PCPP st o <> q1 & p1 <> q1 & o <> q2 & p2 <> q2 & o <> q3 & p3 <> q3 & not o,p1,p2 is_collinear & not o,p1,p3 is_collinear & not o,p2,p3 is_collinear & p1,p2,r3 is_collinear & q1,q2,r3 is_collinear & p2,p3,r1 is_collinear & q2,q3,r1 is_collinear & p1,p3,r2 is_collinear & q1,q3,r2 is_collinear & o,p1,q1 is_collinear & o,p2,q2 is_collinear & o,p3,q3 is_collinear holds r1,r2,r3 is_collinear by Th17; hence PCPP is Desarguesian by ANPROJ_2:def_12; ::_thesis: verum end; now__::_thesis:_(_ex_p,_p1,_q,_q1_being_Element_of_PCPP_st_ for_r_being_Element_of_PCPP_holds_ (_not_p,p1,r_is_collinear_or_not_q,q1,r_is_collinear_)_implies_PCPP_is_Desarguesian_) assume ex p, p1, q, q1 being Element of PCPP st for r being Element of PCPP holds ( not p,p1,r is_collinear or not q,q1,r is_collinear ) ; ::_thesis: PCPP is Desarguesian then PCPP is up-3-dimensional CollProjectiveSpace by ANPROJ_2:def_14; hence PCPP is Desarguesian ; ::_thesis: verum end; hence PCPP is Desarguesian by A2; ::_thesis: verum end; end;