let PCPP be Pappian CollProjectivePlane; :: thesis: for p1, p2, p3, q1, q2, q3, r1, r2, r3 being Element of PCPP st p2 <> p3 & p1 <> p3 & q2 <> q3 & q1 <> q2 & q1 <> q3 & not p1,p2,q1 are_collinear & p1,p2,p3 are_collinear & q1,q2,q3 are_collinear & p1,q2,r3 are_collinear & q1,p2,r3 are_collinear & p1,q3,r2 are_collinear & p3,q1,r2 are_collinear & p2,q3,r1 are_collinear & p3,q2,r1 are_collinear holds
r1,r2,r3 are_collinear
let p1, p2, p3, q1, q2, q3, r1, r2, r3 be Element of PCPP; :: thesis: ( p2 <> p3 & p1 <> p3 & q2 <> q3 & q1 <> q2 & q1 <> q3 & not p1,p2,q1 are_collinear & p1,p2,p3 are_collinear & q1,q2,q3 are_collinear & p1,q2,r3 are_collinear & q1,p2,r3 are_collinear & p1,q3,r2 are_collinear & p3,q1,r2 are_collinear & p2,q3,r1 are_collinear & p3,q2,r1 are_collinear implies r1,r2,r3 are_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 are_collinear and
A7: p1,p2,p3 are_collinear and
A8: q1,q2,q3 are_collinear and
A9: p1,q2,r3 are_collinear and
A10: q1,p2,r3 are_collinear and
A11: p1,q3,r2 are_collinear and
A12: p3,q1,r2 are_collinear and
A13: p2,q3,r1 are_collinear and
A14: p3,q2,r1 are_collinear ; :: thesis: r1,r2,r3 are_collinear
A15: p1 <> p2 by A6, ANPROJ_2:def 7;
A16: now :: thesis: ( not p1,p2,q2 are_collinear implies r1,r2,r3 are_collinear )
assume A17: not p1,p2,q2 are_collinear ; :: thesis: r1,r2,r3 are_collinear
A18: now :: thesis: ( not p1,p2,q3 are_collinear implies r1,r2,r3 are_collinear )
assume A19: not p1,p2,q3 are_collinear ; :: thesis: r1,r2,r3 are_collinear
A20: now :: thesis: ( ( q1,q2,p1 are_collinear or q1,q2,p2 are_collinear or q1,q2,p3 are_collinear ) implies r1,r2,r3 are_collinear )
A21: now :: thesis: ( q1,q2,p2 are_collinear implies r1,r2,r3 are_collinear )
( not p2,p1,q2 are_collinear & p2,p1,p3 are_collinear ) by A7, A17, Th1;
then not p2,p3,q2 are_collinear by A1, Th6;
then A22: not q2,p2,p3 are_collinear by Th1;
assume A23: q1,q2,p2 are_collinear ; :: thesis: r1,r2,r3 are_collinear
then A24: p2,q1,q2 are_collinear by Th1;
( p2 <> q1 & p2,q1,r3 are_collinear ) by A6, A10, Th1, ANPROJ_2:def 7;
then p2,r3,q2 are_collinear by A24, Th2;
then A25: q2,p2,r3 are_collinear by Th1;
( q2,p1,r3 are_collinear & not q2,p1,p2 are_collinear ) by A9, A17, Th1;
then A26: q2 = r3 by A25, Th7;
A27: q2,q1,q3 are_collinear by A8, Th1;
q2,q1,p2 are_collinear by A23, Th1;
then q2,p2,q3 are_collinear by A4, A27, Th2;
then A28: p2,q3,q2 are_collinear by Th1;
p2 <> q3 by A19, ANPROJ_2:def 7;
then p2,r1,q2 are_collinear by A13, A28, Th2;
then A29: q2,p2,r1 are_collinear by Th1;
q2,p3,r1 are_collinear by A14, Th1;
then q2 = r1 by A29, A22, Th7;
hence r1,r2,r3 are_collinear by A26, ANPROJ_2:def 7; :: thesis: verum
end;
A30: now :: thesis: ( q1,q2,p3 are_collinear implies r1,r2,r3 are_collinear )
( not p2,p1,q3 are_collinear & p2,p1,p3 are_collinear ) by A7, A19, Th1;
then not p2,p3,q3 are_collinear by A1, Th6;
then A31: not q3,p2,p3 are_collinear by Th1;
assume A32: q1,q2,p3 are_collinear ; :: thesis: r1,r2,r3 are_collinear
then A33: q2,q1,p3 are_collinear by Th1;
q2,q1,q3 are_collinear by A8, Th1;
then q2,q3,p3 are_collinear by A4, A33, Th2;
then p3,q2,q3 are_collinear by Th1;
then p3,r1,q3 are_collinear by A7, A14, A17, Th2;
then A34: q3,p3,r1 are_collinear by Th1;
not p1,p3,q3 are_collinear by A2, A7, A19, Th6;
then A35: not q3,p1,p3 are_collinear by Th1;
q1,q3,p3 are_collinear by A4, A8, A32, Th2;
then p3,q1,q3 are_collinear by Th1;
then p3,r2,q3 are_collinear by A6, A7, A12, Th2;
then A36: q3,p3,r2 are_collinear by Th1;
q3,p2,r1 are_collinear by A13, Th1;
then A37: q3 = r1 by A34, A31, Th7;
q3,p1,r2 are_collinear by A11, Th1;
then q3 = r2 by A36, A35, Th7;
hence r1,r2,r3 are_collinear by A37, ANPROJ_2:def 7; :: thesis: verum
end;
A38: now :: thesis: ( q1,q2,p1 are_collinear implies r1,r2,r3 are_collinear )
not p1,p3,q1 are_collinear by A2, A6, A7, Th6;
then A39: not q1,p1,p3 are_collinear by Th1;
assume A40: q1,q2,p1 are_collinear ; :: thesis: r1,r2,r3 are_collinear
then q1,p1,q3 are_collinear by A4, A8, Th2;
then A41: p1,q3,q1 are_collinear by Th1;
p1 <> q3 by A19, ANPROJ_2:def 7;
then p1,r2,q1 are_collinear by A11, A41, Th2;
then A42: q1,p1,r2 are_collinear by Th1;
A43: p1 <> q2 by A17, ANPROJ_2:def 7;
p1,q2,q1 are_collinear by A40, Th1;
then p1,r3,q1 are_collinear by A9, A43, Th2;
then A44: q1,p1,r3 are_collinear by Th1;
not q1,p2,p1 are_collinear by A6, Th1;
then A45: q1 = r3 by A10, A44, Th7;
q1,p3,r2 are_collinear by A12, Th1;
then q1 = r2 by A42, A39, Th7;
hence r1,r2,r3 are_collinear by A45, ANPROJ_2:def 7; :: thesis: verum
end;
assume ( q1,q2,p1 are_collinear or q1,q2,p2 are_collinear or q1,q2,p3 are_collinear ) ; :: thesis: r1,r2,r3 are_collinear
hence r1,r2,r3 are_collinear by A38, A21, A30; :: thesis: verum
end;
now :: thesis: ( not q1,q2,p1 are_collinear & not q1,q2,p2 are_collinear & not q1,q2,p3 are_collinear implies r1,r2,r3 are_collinear )
assume that
A46: not q1,q2,p1 are_collinear and
A47: ( not q1,q2,p2 are_collinear & not q1,q2,p3 are_collinear ) ; :: thesis: r1,r2,r3 are_collinear
consider o being Element of PCPP such that
A48: p1,p2,o are_collinear and
A49: q1,q2,o are_collinear by ANPROJ_2:def 14;
not p1,o,q1 are_collinear by A6, A46, A48, A49, Th6;
then A50: not o,p1,q1 are_collinear by Th1;
q1,q3,o are_collinear by A4, A8, A49, Th2;
then A51: o,q1,q3 are_collinear by Th1;
p1,p3,o are_collinear by A7, A15, A48, Th2;
then A52: o,p1,p3 are_collinear by Th1;
( o,p1,p2 are_collinear & o,q1,q2 are_collinear ) by A48, A49, Th1;
hence r1,r2,r3 are_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 are_collinear by A20; :: thesis: verum
end;
now :: thesis: ( p1,p2,q3 are_collinear implies r1,r2,r3 are_collinear )
assume A53: p1,p2,q3 are_collinear ; :: thesis: r1,r2,r3 are_collinear
A54: now :: thesis: ( p2 <> q3 & p1 <> q3 implies r1,r2,r3 are_collinear )
assume that
A55: p2 <> q3 and
A56: p1 <> q3 ; :: thesis: r1,r2,r3 are_collinear
p1,q3,p2 are_collinear by A53, Th1;
then p1,p2,r2 are_collinear by A11, A56, Th2;
then p1,r2,p3 are_collinear by A7, A15, Th2;
then A57: p3,p1,r2 are_collinear by Th1;
not p1,p3,q1 are_collinear by A2, A6, A7, Th6;
then not p3,q1,p1 are_collinear by Th1;
then A58: p3 = r2 by A12, A57, Th7;
A59: p2,p1,p3 are_collinear by A7, Th1;
p2,q3,p1 are_collinear by A53, Th1;
then p2,p1,r1 are_collinear by A13, A55, Th2;
then p2,r1,p3 are_collinear by A15, A59, Th2;
then A60: p3,p2,r1 are_collinear by Th1;
( not p2,p1,q2 are_collinear & p2,p1,p3 are_collinear ) by A7, A17, Th1;
then not p2,p3,q2 are_collinear by A1, Th6;
then not p3,q2,p2 are_collinear by Th1;
then p3 = r1 by A14, A60, Th7;
hence r1,r2,r3 are_collinear by A58, ANPROJ_2:def 7; :: thesis: verum
end;
A61: now :: thesis: ( p2 = q3 implies r1,r2,r3 are_collinear )
not p1,p3,q1 are_collinear by A2, A6, A7, Th6;
then A62: not p3,p1,q1 are_collinear by Th1;
A63: not p2,q1,p1 are_collinear by A6, Th1;
A64: p2,q1,r3 are_collinear by A10, Th1;
assume A65: p2 = q3 ; :: thesis: r1,r2,r3 are_collinear
then p2,q1,q2 are_collinear by A8, Th1;
then p2,q2,r3 are_collinear by A5, A65, A64, Th2;
then A66: q2,p2,r3 are_collinear by Th1;
p2,q1,q2 are_collinear by A8, A65, Th1;
then not p2,q2,p1 are_collinear by A3, A65, A63, Th6;
then A67: not q2,p1,p2 are_collinear by Th1;
p1,p3,r2 are_collinear by A7, A11, A15, A65, Th2;
then p3,p1,r2 are_collinear by Th1;
then A68: p3 = r2 by A12, A62, Th7;
q2,p1,r3 are_collinear by A9, Th1;
then q2 = r3 by A66, A67, Th7;
hence r1,r2,r3 are_collinear by A14, A68, Th1; :: thesis: verum
end;
hence r1,r2,r3 are_collinear by A61, A54; :: thesis: verum
end;
hence r1,r2,r3 are_collinear by A18; :: thesis: verum
end;
now :: thesis: ( p1,p2,q2 are_collinear implies r1,r2,r3 are_collinear )
A73: now :: thesis: ( p1 = q2 implies r1,r2,r3 are_collinear )
not p1,p3,q1 are_collinear by A2, A6, A7, Th6;
then A74: not q1,p1,p3 are_collinear by Th1;
A75: not p1,q1,p2 are_collinear by A6, Th1;
assume A76: p1 = q2 ; :: thesis: r1,r2,r3 are_collinear
then p1,q3,q1 are_collinear by A8, Th1;
then p1,q1,r2 are_collinear by A3, A11, A76, Th2;
then A77: q1,p1,r2 are_collinear by Th1;
A78: p1,p3,p2 are_collinear by A7, Th1;
p1,p3,r1 are_collinear by A14, A76, Th1;
then p1,p2,r1 are_collinear by A2, A78, Th2;
then A79: p2,p1,r1 are_collinear by Th1;
q1,p3,r2 are_collinear by A12, Th1;
then A80: q1 = r2 by A77, A74, Th7;
p1,q1,q3 are_collinear by A8, A76, Th1;
then not p1,q3,p2 are_collinear by A3, A76, A75, Th6;
then not p2,p1,q3 are_collinear by Th1;
then r1 = p2 by A13, A79, Th7;
hence r1,r2,r3 are_collinear by A10, A80, Th1; :: thesis: verum
end;
assume A81: p1,p2,q2 are_collinear ; :: thesis: r1,r2,r3 are_collinear
A82: now :: thesis: ( p1 <> q2 & p3 <> q2 implies r1,r2,r3 are_collinear )
assume that
A83: p1 <> q2 and
A84: p3 <> q2 ; :: thesis: r1,r2,r3 are_collinear
p1,q2,p2 are_collinear by A81, Th1;
then p1,p2,r3 are_collinear by A9, A83, Th2;
then A85: p2,p1,r3 are_collinear by Th1;
p1,q2,p3 are_collinear by A7, A15, A81, Th2;
then p3,q2,p1 are_collinear by Th1;
then p3,p1,r1 are_collinear by A14, A84, Th2;
then A86: p1,p3,r1 are_collinear by Th1;
p1,p3,p2 are_collinear by A7, Th1;
then p1,p2,r1 are_collinear by A2, A86, Th2;
then A87: p2,p1,r1 are_collinear by Th1;
not p2,p1,q3 are_collinear by A3, A6, A8, A81, Th11;
then A88: p2 = r1 by A13, A87, Th7;
( not p2,p1,q1 are_collinear & p2,q1,r3 are_collinear ) by A6, A10, Th1;
then p2 = r3 by A85, Th7;
hence r1,r2,r3 are_collinear by A88, ANPROJ_2:def 7; :: thesis: verum
end;
now :: thesis: ( p3 = q2 implies r1,r2,r3 are_collinear )
assume A89: p3 = q2 ; :: thesis: r1,r2,r3 are_collinear
then q1,q3,p3 are_collinear by A8, Th1;
then A90: not q3,p1,q1 are_collinear by A2, A5, A6, A7, Th10;
p1,p3,p2 are_collinear by A7, Th1;
then p1,p2,r3 are_collinear by A2, A9, A89, Th2;
then A91: p2,p1,r3 are_collinear by Th1;
( not p2,p1,q1 are_collinear & p2,q1,r3 are_collinear ) by A6, A10, Th1;
then A92: p2 = r3 by A91, Th7;
q1,q2,r2 are_collinear by A12, A89, Th1;
then q1,q3,r2 are_collinear by A4, A8, Th2;
then A93: q3,q1,r2 are_collinear by Th1;
q3,p1,r2 are_collinear by A11, Th1;
then r3,r2,r1 are_collinear by A13, A92, A90, A93, Th7;
hence r1,r2,r3 are_collinear by Th1; :: thesis: verum
end;
hence r1,r2,r3 are_collinear by A73, A82; :: thesis: verum
end;
hence r1,r2,r3 are_collinear by A16; :: thesis: verum