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 & a1 <> b1 & o <> b2 & a2 <> b2 & o <> b3 & a3 <> b3 ) and
A2: ( not o,a1,a2 is_collinear & not o,a1,a3 is_collinear & not o,a2,a3 is_collinear ) and
A3: not o,c1,c3 is_collinear and
A4: ( 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 ) and
A5: ( o,a1,b1 is_collinear & o,a2,b2 is_collinear & o,a3,b3 is_collinear ) and
A6: ( o,a2,x is_collinear & a1,a3,x is_collinear ) and
A7: not c1,c3,x is_collinear ; :: thesis: c1,c2,c3 is_collinear
A8: ( o <> a1 & o <> a2 & a1 <> a2 & o <> a3 & a1 <> a3 & a2 <> a3 ) by A2, ANPROJ_2:def 7;
A9: not a1,a3,b1 is_collinear

proof

( not a1,o,a3 is_collinear & a1,o,b1 is_collinear ) by A2, A5, Th3;
then not a1,b1,a3 is_collinear by A1, Th8;
hence not a1,a3,b1 is_collinear by Th3; :: thesis: verum

end;

A10: ( b1 <> b2 & b1 <> b3 & b2 <> b3 ) by A1, A2, A5, Th9;

A11: now

assume A12: ( a1,a2,a3 is_collinear or b1,b2,b3 is_collinear ) ; :: thesis: c1,c2,c3 is_collinear

A13: now

assume A14: a1,a2,a3 is_collinear ; :: thesis: c1,c2,c3 is_collinear
thus c1,c2,c3 is_collinear :: thesis: verum

proof

A15: a1,a2,c1 is_collinear

proof

a2,a3,a1 is_collinear by A14, Th3;
then a2,a1,c1 is_collinear by A4, A8, Th4;
hence a1,a2,c1 is_collinear by Th3; :: thesis: verum

end;

a1,a2,c2 is_collinear

proof

a1,a3,a2 is_collinear by A14, Th3;
hence a1,a2,c2 is_collinear by A4, A8, Th4; :: thesis: verum

end;

hence c1,c2,c3 is_collinear by A4, A8, A15, ANPROJ_2:def 8; :: thesis: verum

end;

end;

now

assume A16: b1,b2,b3 is_collinear ; :: thesis: c1,c2,c3 is_collinear
thus c1,c2,c3 is_collinear :: thesis: verum

proof

A17: b1,b2,c1 is_collinear

proof

b2,b3,b1 is_collinear by A16, Th3;
then b2,b1,c1 is_collinear by A4, A10, Th4;
hence b1,b2,c1 is_collinear by Th3; :: thesis: verum

end;

b1,b2,c2 is_collinear

proof

b1,b3,b2 is_collinear by A16, Th3;
hence b1,b2,c2 is_collinear by A4, A10, Th4; :: thesis: verum

end;

hence c1,c2,c3 is_collinear by A4, A10, A17, ANPROJ_2:def 8; :: thesis: verum

end;

end;

hence c1,c2,c3 is_collinear by A12, A13; :: thesis: verum

end;

now

assume A18: ( not a1,a2,a3 is_collinear & not b1,b2,b3 is_collinear ) ; :: thesis: c1,c2,c3 is_collinear
assume A19: not c1,c2,c3 is_collinear ; :: thesis: contradiction
A20: ( b1 <> b2 & b1 <> b3 & b2 <> b3 ) by A18, ANPROJ_2:def 7;
consider z being Element of PCPP such that
A21: ( a1,a3,z is_collinear & c1,c3,z is_collinear ) by ANPROJ_2:def 14;
consider p being Element of PCPP such that
A22: ( o,z,p is_collinear & a2,a3,p is_collinear ) by ANPROJ_2:def 14;
consider q being Element of PCPP such that
A23: ( o,a1,q is_collinear & p,c3,q is_collinear ) by ANPROJ_2:def 14;
consider r being Element of PCPP such that
A24: ( p,b2,r is_collinear & q,a3,r is_collinear ) by ANPROJ_2:def 14;
consider a being Element of PCPP such that
A25: ( c1,c3,a is_collinear & o,a2,a is_collinear ) by ANPROJ_2:def 14;
consider q' being Element of PCPP such that
A26: ( o,a1,q' is_collinear & a,a3,q' is_collinear ) by ANPROJ_2:def 14;
consider z' being Element of PCPP such that
A27: ( b1,r,z' is_collinear & o,p,z' is_collinear ) by ANPROJ_2:def 14;
consider z'' being Element of PCPP such that
A28: ( b3,r,z'' is_collinear & o,p,z'' is_collinear ) by ANPROJ_2:def 14;
A29: ( a1 <> c3 & a2 <> c3 & a2 <> c1 & a3 <> c1 & c1 <> c3 )

proof

A30: a1 <> c3

proof

( not o,a2,a1 is_collinear & a2,a1,c3 is_collinear & b2,b1,c3 is_collinear ) by A2, A4, Th3;
hence a1 <> c3 by A1, A5, Th10; :: thesis: verum

end;

( not o,a3,a2 is_collinear & b3,b2,c1 is_collinear & a3,a2,c1 is_collinear ) by A2, A4, Th3;
hence ( a1 <> c3 & a2 <> c3 & a2 <> c1 & a3 <> c1 & c1 <> c3 ) by A1, A2, A3, A4, A5, A30, Th10, ANPROJ_2:def 7; :: thesis: verum

end;

A31: o <> p by A2, A22, Th3;
A32: a <> c1

proof

not a2,a3,o is_collinear by A2, Th3;
then not a2,c1,o is_collinear by A4, A29, Th8;
hence a <> c1 by A25, Th3; :: thesis: verum

end;

A33: ( o <> a & a2 <> a & o <> a2 & a1 <> a3 & a1 <> z & a3 <> z )

proof

A34: a2 <> c3 by A1, A2, A4, A5, Th10;
A35: c1 <> c3 by A3, ANPROJ_2:def 7;
( not o,a3,a2 is_collinear & b3,b2,c1 is_collinear & a3,a2,c1 is_collinear ) by A2, A4, Th3;
then A36: a2 <> c1 by A1, A5, Th10;
A37: a2 <> a

proof

assume A38: not a2 <> a ; :: thesis: contradiction
then ( c3,a2,c1 is_collinear & c3,a2,a1 is_collinear & c1,a2,c3 is_collinear & c1,a2,a3 is_collinear ) by A4, A25, Th3;
then ( c3,c1,a1 is_collinear & c1,c3,a3 is_collinear ) by A34, A36, Th4;
then ( c1,c3,a1 is_collinear & c1,c3,a3 is_collinear ) by Th3;
hence contradiction by A18, A25, A35, A38, ANPROJ_2:def 8; :: thesis: verum

end;

( not o,a2,a1 is_collinear & a2,a1,c3 is_collinear & b2,b1,c3 is_collinear ) by A2, A4, Th3;
then A39: a1 <> c3 by A1, A5, Th10;
a3 <> c1 by A1, A2, A4, A5, Th10;
hence ( o <> a & a2 <> a & o <> a2 & a1 <> a3 & a1 <> z & a3 <> z ) by A2, A3, A4, A18, A21, A25, A34, A36, A37, A39, Th3, Th12, ANPROJ_2:def 7; :: thesis: verum

end;

not a1,a2,o is_collinear by A2, Th3;
then not a1,c3,o is_collinear by A4, A29, Th8;
then A40: not o,a1,c3 is_collinear by Th3;
a2,b2,o is_collinear by A5, Th3;
then A41: not b1,o,b2 is_collinear by A1, A2, A5, Th16;
then A42: not o,b1,b2 is_collinear by Th3;
A43: not o,a,a3 is_collinear by A2, A25, A33, Th8;
A44: ( b1 <> b2 & b1 <> p & b2 <> p )

proof

A45: b1 <> p

proof

not a1,a3,o is_collinear by A2, Th3;
then not a1,z,o is_collinear by A21, A33, Th8;
then not o,z,a1 is_collinear by Th3;
then not o,p,a1 is_collinear by A22, A31, Th8;
hence b1 <> p by A5, Th3; :: thesis: verum

end;

( a2,o,b2 is_collinear & not a2,o,a3 is_collinear ) by A2, A5, Th3;
then not a2,b2,a3 is_collinear by A1, Th8;
hence ( b1 <> b2 & b1 <> p & b2 <> p ) by A18, A22, A45, Th3, ANPROJ_2:def 7; :: thesis: verum

end;

( not a2,a1,o is_collinear & a2,a1,c3 is_collinear ) by A2, A4, Th3;
then not a2,c3,o is_collinear by A29, Th8;
then A46: a <> c3 by A25, Th3;
A47: a3,a,q is_collinear

proof

A48: ( a3,z,a1 is_collinear & a3,a2,p is_collinear ) by A21, A22, Th3;
A49: a2,a1,c3 is_collinear by A4, Th3;
a,z,c3 is_collinear

proof

A50: ( c3,c1,z is_collinear & c3,c1,a is_collinear ) by A21, A25, Th3;
c1 <> c3 by A3, ANPROJ_2:def 7;
then c3,a,z is_collinear by A50, Th4;
hence a,z,c3 is_collinear by Th3; :: thesis: verum

end;

then c3,q',p is_collinear by A2, A22, A25, A26, A33, A48, A49, Th20;
then A51: p,c3,q' is_collinear by Th3;
( not a2,a1,a3 is_collinear & a2,a1,c3 is_collinear & a2 <> c3 ) by A4, A18, A29, Th3;
then not a2,c3,a3 is_collinear by Th8;
then A52: p <> c3 by A22, Th3;
( not a1,a3,o is_collinear & a1,a3,z is_collinear & a1 <> z ) by A2, A21, A33, Th3;
then not a1,z,o is_collinear by Th8;
then not o,z,a1 is_collinear by Th3;
then not o,p,a1 is_collinear by A22, A31, Th8;
then not o,a1,p is_collinear by Th3;
then a,a3,q is_collinear by A8, A23, A26, A51, A52, Th17;
hence a3,a,q is_collinear by Th3; :: thesis: verum

end;

A53: not a3,q,o is_collinear

proof

not a3,a,o is_collinear by A43, Th3;
hence not a3,q,o is_collinear by A2, A23, A47, Th8; :: thesis: verum

end;

A54: not o,b2,b3 is_collinear

proof

a3,b3,o is_collinear by A5, Th3;
then not b2,o,b3 is_collinear by A1, A2, A5, Th16;
hence not o,b2,b3 is_collinear by Th3; :: thesis: verum

end;

A55: ( b2 <> c1 & b2 <> c3 )

proof

A56: ( o,b1,a1 is_collinear & o,b2,a2 is_collinear ) by A5, Th3;
A57: ( o,b2,a2 is_collinear & o,b3,a3 is_collinear ) by A5, Th3;
A58: not o,b3,b2 is_collinear by A54, Th3;
( b3,b2,c1 is_collinear & a3,a2,c1 is_collinear ) by A4, Th3;
hence ( b2 <> c1 & b2 <> c3 ) by A1, A4, A8, A42, A56, A57, A58, Th10; :: thesis: verum

end;

A59: a <> b2

proof

assume A60: not a <> b2 ; :: thesis: contradiction
then A61: c1,b2,c3 is_collinear by A25, Th3;
c1,b2,b3 is_collinear by A4, Th3;
then A62: c1,c3,b3 is_collinear by A55, A61, Th4;
A63: c3,b2,b1 is_collinear by A4, Th3;
c3,b2,c1 is_collinear by A25, A60, Th3;
then c3,c1,b1 is_collinear by A55, A63, Th4;
then c1,c3,b1 is_collinear by Th3;
hence contradiction by A18, A25, A29, A60, A62, ANPROJ_2:def 8; :: thesis: verum

end;

A64: not a,b2,a3 is_collinear

proof

A65: not a,o,a3 is_collinear by A43, Th3;
o,a,b2 is_collinear by A5, A8, A25, Th4;
then a,o,b2 is_collinear by Th3;
hence not a,b2,a3 is_collinear by A59, A65, Th8; :: thesis: verum

end;

A66: a3,r,a is_collinear

proof

( a3,q,a is_collinear & a3,q,r is_collinear ) by A24, A47, Th3;
hence a3,r,a is_collinear by A2, A23, Th4; :: thesis: verum

end;

then A67: b2 <> r by A64, Th3;
A68: a <> a2

proof

assume A69: not a <> a2 ; :: thesis: contradiction
then ( c1,a2,c3 is_collinear & c1,a2,a3 is_collinear ) by A4, A25, Th3;
then A70: c1,c3,a3 is_collinear by A29, Th4;
( c3,a2,a1 is_collinear & c3,a2,c1 is_collinear ) by A4, A25, A69, Th3;
then c3,c1,a1 is_collinear by A29, Th4;
then c1,c3,a1 is_collinear by Th3;
hence contradiction by A18, A25, A29, A69, A70, ANPROJ_2:def 8; :: thesis: verum

end;

A71: not a3,o,b2 is_collinear

proof

not o,b2,a3 is_collinear by A1, A2, A5, Th8;
hence not a3,o,b2 is_collinear by Th3; :: thesis: verum

end;

thus contradiction :: thesis: verum

proof

A72: not p,o,a is_collinear

proof

o <> x by A2, A6, Th3;
then not o,x,a3 is_collinear by A2, A6, Th8;
then A73: not x,a3,o is_collinear by Th3;
( a3,a1,z is_collinear & a3,a1,x is_collinear ) by A6, A21, Th3;
then a3,x,z is_collinear by A33, Th4;
then x,a3,z is_collinear by Th3;
then not x,z,o is_collinear by A7, A21, A73, Th8;
then not o,z,x is_collinear by Th3;
then not o,p,x is_collinear by A22, A31, Th8;
then A74: not o,x,p is_collinear by Th3;
o,x,a is_collinear by A6, A8, A25, Th4;
then not o,a,p is_collinear by A33, A74, Th8;
hence not p,o,a is_collinear by Th3; :: thesis: verum

end;

A75: a3 <> p

proof

assume not a3 <> p ; :: thesis: contradiction
then A76: a3,o,z is_collinear by A22, Th3;
( a3,a1,z is_collinear & not a3,o,a1 is_collinear ) by A2, A21, Th3;
hence contradiction by A33, A76, Th9; :: thesis: verum

end;

A77: not a,a3,p is_collinear

proof

( not a,o,p is_collinear & a,o,a2 is_collinear ) by A25, A72, Th3;
then not a,a2,p is_collinear by A68, Th8;
then A78: not p,a2,a is_collinear by Th3;
p,a2,a3 is_collinear by A22, Th3;
then not p,a3,a is_collinear by A75, A78, Th8;
hence not a,a3,p is_collinear by Th3; :: thesis: verum

end;

then A79: p <> r by A66, Th3;
A80: z <> r

proof

A81: o,a,b2 is_collinear by A5, A8, A25, Th4;
not o,a,p is_collinear by A72, Th3;
then not o,b2,p is_collinear by A1, A81, Th8;
then not p,b2,o is_collinear by Th3;
then not p,r,o is_collinear by A24, A79, Th8;
hence z <> r by A22, Th3; :: thesis: verum

end;

A82: now

assume A83: b1 = q ; :: thesis: contradiction
consider z' being Element of PCPP such that
A84: ( b1,b3,z' is_collinear & p,o,z' is_collinear ) by ANPROJ_2:def 14;
( b1,c3,p is_collinear & b1,c3,b2 is_collinear ) by A4, A23, A83, Th3;
then A85: b1,b2,p is_collinear by A5, A40, Th4;
A86: not b1,b2,o is_collinear

proof

( not o,a1,a2 is_collinear & o,a1,b1 is_collinear & a2,b2,o is_collinear & o <> b1 & o <> b2 ) by A1, A2, A5, Th3;
then not b1,o,b2 is_collinear by Th16;
hence not b1,b2,o is_collinear by Th3; :: thesis: verum

end;

( b1,a3,a is_collinear & o,b2,a is_collinear & b1,b3,z' is_collinear & p,o,z' is_collinear & b2,b3,c1 is_collinear & p,a3,c1 is_collinear )

proof

( a3,a2,c1 is_collinear & a3,a2,p is_collinear ) by A4, A22, Th3;
then a3,c1,p is_collinear by A8, Th4;
hence ( b1,a3,a is_collinear & o,b2,a is_collinear & b1,b3,z' is_collinear & p,o,z' is_collinear & b2,b3,c1 is_collinear & p,a3,c1 is_collinear ) by A4, A5, A25, A33, A47, A83, A84, Th3, Th4; :: thesis: verum

end;

then c1,z',a is_collinear by A1, A5, A8, A44, A85, A86, Th20;
then A87: a,c1,z' is_collinear by Th3;
c1,a,z is_collinear by A21, A25, A29, Th4;
then A88: a,c1,z is_collinear by Th3;
p,o,z is_collinear by A22, Th3;
then A89: b1,b3,z is_collinear by A31, A32, A72, A84, A87, A88, Th17;
A90: not a1,o,a3 is_collinear by A2, Th3;
a1,o,b1 is_collinear by A5, Th3;
then not a1,b1,a3 is_collinear by A1, A90, Th8;
then not a1,a3,b1 is_collinear by Th3;
then c1,c3,c2 is_collinear by A4, A8, A20, A21, A89, Th17;
hence contradiction by A19, Th3; :: thesis: verum

end;

now

assume A91: b1 <> q ; :: thesis: contradiction
A92: ( q <> o & b1 <> o & b2 <> p & b2 <> r & p <> r ) by A1, A44, A53, A64, A66, A77, Th3, ANPROJ_2:def 7;
A93: not q,b1,b2 is_collinear

proof

o,b1,q is_collinear by A5, A8, A23, Th4;
then b1,o,q is_collinear by Th3;
then not b1,q,b2 is_collinear by A41, A91, Th8;
hence not q,b1,b2 is_collinear by Th3; :: thesis: verum

end;

A94: ( q,b1,o is_collinear & b2,p,r is_collinear )

proof

o,b1,q is_collinear by A5, A8, A23, Th4;
hence ( q,b1,o is_collinear & b2,p,r is_collinear ) by A24, Th3; :: thesis: verum

end;

( q,p,c3 is_collinear & b2,b1,c3 is_collinear & q,r,a is_collinear & o,b2,a is_collinear & b1,r,z' is_collinear & o,p,z' is_collinear )

proof

q,r,a is_collinear

proof

( q,a3,a is_collinear & q,a3,r is_collinear ) by A24, A47, Th3;
hence q,r,a is_collinear by A2, A23, Th4; :: thesis: verum

end;

hence ( q,p,c3 is_collinear & b2,b1,c3 is_collinear & q,r,a is_collinear & o,b2,a is_collinear & b1,r,z' is_collinear & o,p,z' is_collinear ) by A4, A5, A8, A23, A25, A27, Th3, Th4; :: thesis: verum

end;

then A95: z',a,c3 is_collinear by A92, A93, A94, Th20;
( c3,c1,z is_collinear & c3,c1,a is_collinear ) by A21, A25, Th3;
then c3,z,a is_collinear by A29, Th4;
then A96: a,c3,z is_collinear by Th3;
A97: a,c3,z' is_collinear by A95, Th3;
A98: o,p,z is_collinear by A22, Th3;
not o,p,a is_collinear by A72, Th3;
then A99: b1,r,z is_collinear by A27, A31, A46, A96, A97, A98, Th17;
A100: a3,o,b3 is_collinear by A5, Th3;
A101: b2,r,p is_collinear by A24, Th3;
o,a,b2 is_collinear by A5, A8, A25, Th4;
then A102: b2,o,a is_collinear by Th3;
( a3,a2,c1 is_collinear & a3,a2,p is_collinear ) by A4, A22, Th3;
then A103: a3,p,c1 is_collinear by A8, Th4;
b3,b2,c1 is_collinear by A4, Th3;
then z'',c1,a is_collinear by A1, A28, A44, A66, A67, A71, A79, A100, A101, A102, A103, Th20;
then ( c1,a,z'' is_collinear & c1,a,c3 is_collinear ) by A25, Th3;
then A104: c1,c3,z'' is_collinear by A32, Th4;
A105: not c1,c3,o is_collinear by A3, Th3;
o,p,z is_collinear by A22, Th3;
then b3,r,z is_collinear by A21, A28, A29, A31, A104, A105, Th17;
then ( z,r,b1 is_collinear & z,r,b3 is_collinear ) by A99, Th3;
then z,b1,b3 is_collinear by A80, Th4;
then b1,b3,z is_collinear by Th3;
then c1,c3,c2 is_collinear by A4, A8, A9, A20, A21, Th17;
hence contradiction by A19, Th3; :: thesis: verum

end;

hence contradiction by A82; :: thesis: verum

end;

end;

hence c1,c2,c3 is_collinear by A11; :: thesis: verum