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

assume A17: not p1,p2,q2 is_collinear ; :: thesis: r1,r2,r3 is_collinear

A18: now

assume A19: not p1,p2,q3 is_collinear ; :: thesis: r1,r2,r3 is_collinear

A20: now

A21: now

( not p2,p1,q2 is_collinear & p2,p1,p3 is_collinear ) by A7, A17, Th3;
then not p2,p3,q2 is_collinear by A1, Th8;
then A22: not q2,p2,p3 is_collinear by Th3;
assume A23: q1,q2,p2 is_collinear ; :: thesis: r1,r2,r3 is_collinear
then A24: p2,q1,q2 is_collinear by Th3;
( p2 <> q1 & p2,q1,r3 is_collinear ) by A6, A10, Th3, ANPROJ_2:def 7;
then p2,r3,q2 is_collinear by A24, Th4;
then A25: q2,p2,r3 is_collinear by Th3;
( q2,p1,r3 is_collinear & not q2,p1,p2 is_collinear ) by A9, A17, Th3;
then A26: q2 = r3 by A25, Th9;
A27: q2,q1,q3 is_collinear by A8, Th3;
q2,q1,p2 is_collinear by A23, Th3;
then q2,p2,q3 is_collinear by A4, A27, Th4;
then A28: p2,q3,q2 is_collinear by Th3;
p2 <> q3 by A19, ANPROJ_2:def 7;
then p2,r1,q2 is_collinear by A13, A28, Th4;
then A29: q2,p2,r1 is_collinear by Th3;
q2,p3,r1 is_collinear by A14, Th3;
then q2 = r1 by A29, A22, Th9;
hence r1,r2,r3 is_collinear by A26, ANPROJ_2:def 7; :: thesis: verum

end;

A30: now

( not p2,p1,q3 is_collinear & p2,p1,p3 is_collinear ) by A7, A19, Th3;
then not p2,p3,q3 is_collinear by A1, Th8;
then A31: not q3,p2,p3 is_collinear by Th3;
assume A32: q1,q2,p3 is_collinear ; :: thesis: r1,r2,r3 is_collinear
then A33: q2,q1,p3 is_collinear by Th3;
q2,q1,q3 is_collinear by A8, Th3;
then q2,q3,p3 is_collinear by A4, A33, Th4;
then p3,q2,q3 is_collinear by Th3;
then p3,r1,q3 is_collinear by A7, A14, A17, Th4;
then A34: q3,p3,r1 is_collinear by Th3;
not p1,p3,q3 is_collinear by A2, A7, A19, Th8;
then A35: not q3,p1,p3 is_collinear by Th3;
q1,q3,p3 is_collinear by A4, A8, A32, Th4;
then p3,q1,q3 is_collinear by Th3;
then p3,r2,q3 is_collinear by A6, A7, A12, Th4;
then A36: q3,p3,r2 is_collinear by Th3;
q3,p2,r1 is_collinear by A13, Th3;
then A37: q3 = r1 by A34, A31, Th9;
q3,p1,r2 is_collinear by A11, Th3;
then q3 = r2 by A36, A35, Th9;
hence r1,r2,r3 is_collinear by A37, ANPROJ_2:def 7; :: thesis: verum

end;

A38: now

not p1,p3,q1 is_collinear by A2, A6, A7, Th8;
then A39: not q1,p1,p3 is_collinear by Th3;
assume A40: q1,q2,p1 is_collinear ; :: thesis: r1,r2,r3 is_collinear
then q1,p1,q3 is_collinear by A4, A8, Th4;
then A41: p1,q3,q1 is_collinear by Th3;
p1 <> q3 by A19, ANPROJ_2:def 7;
then p1,r2,q1 is_collinear by A11, A41, Th4;
then A42: q1,p1,r2 is_collinear by Th3;
A43: p1 <> q2 by A17, ANPROJ_2:def 7;
p1,q2,q1 is_collinear by A40, Th3;
then p1,r3,q1 is_collinear by A9, A43, Th4;
then A44: q1,p1,r3 is_collinear by Th3;
not q1,p2,p1 is_collinear by A6, Th3;
then A45: q1 = r3 by A10, A44, Th9;
q1,p3,r2 is_collinear by A12, Th3;
then q1 = r2 by A42, A39, Th9;
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

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, Th8;
then A50: not o,p1,q1 is_collinear by Th3;
q1,q3,o is_collinear by A4, A8, A49, Th4;
then A51: o,q1,q3 is_collinear by Th3;
p1,p3,o is_collinear by A7, A15, A48, Th4;
then A52: o,p1,p3 is_collinear by Th3;
( o,p1,p2 is_collinear & o,q1,q2 is_collinear ) by A48, A49, Th3;
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

assume A53: p1,p2,q3 is_collinear ; :: thesis: r1,r2,r3 is_collinear

A54: now

assume that
A55: p2 <> q3 and
A56: p1 <> q3 ; :: thesis: r1,r2,r3 is_collinear
p1,q3,p2 is_collinear by A53, Th3;
then p1,p2,r2 is_collinear by A11, A56, Th4;
then p1,r2,p3 is_collinear by A7, A15, Th4;
then A57: p3,p1,r2 is_collinear by Th3;
not p1,p3,q1 is_collinear by A2, A6, A7, Th8;
then not p3,q1,p1 is_collinear by Th3;
then A58: p3 = r2 by A12, A57, Th9;
A59: p2,p1,p3 is_collinear by A7, Th3;
p2,q3,p1 is_collinear by A53, Th3;
then p2,p1,r1 is_collinear by A13, A55, Th4;
then p2,r1,p3 is_collinear by A15, A59, Th4;
then A60: p3,p2,r1 is_collinear by Th3;
( not p2,p1,q2 is_collinear & p2,p1,p3 is_collinear ) by A7, A17, Th3;
then not p2,p3,q2 is_collinear by A1, Th8;
then not p3,q2,p2 is_collinear by Th3;
then p3 = r1 by A14, A60, Th9;
hence r1,r2,r3 is_collinear by A58, ANPROJ_2:def 7; :: thesis: verum

end;

A61: now

not p1,p3,q1 is_collinear by A2, A6, A7, Th8;
then A62: not p3,p1,q1 is_collinear by Th3;
A63: not p2,q1,p1 is_collinear by A6, Th3;
A64: p2,q1,r3 is_collinear by A10, Th3;
assume A65: p2 = q3 ; :: thesis: r1,r2,r3 is_collinear
then p2,q1,q2 is_collinear by A8, Th3;
then p2,q2,r3 is_collinear by A5, A65, A64, Th4;
then A66: q2,p2,r3 is_collinear by Th3;
p2,q1,q2 is_collinear by A8, A65, Th3;
then not p2,q2,p1 is_collinear by A3, A65, A63, Th8;
then A67: not q2,p1,p2 is_collinear by Th3;
p1,p3,r2 is_collinear by A7, A11, A15, A65, Th4;
then p3,p1,r2 is_collinear by Th3;
then A68: p3 = r2 by A12, A62, Th9;
q2,p1,r3 is_collinear by A9, Th3;
then q2 = r3 by A66, A67, Th9;
hence r1,r2,r3 is_collinear by A14, A68, Th3; :: thesis: verum

end;

now

assume A69: p1 = q3 ; :: thesis: r1,r2,r3 is_collinear
then p1,p2,r1 is_collinear by A13, Th3;
then p1,p3,r1 is_collinear by A7, A15, Th4;
then A70: p3,p1,r1 is_collinear by Th3;
p1,q2,q1 is_collinear by A8, A69, Th3;
then p1,q1,r3 is_collinear by A3, A9, A69, Th4;
then A71: q1,p1,r3 is_collinear by Th3;
not p3,p1,q2 is_collinear by A2, A3, A6, A7, A8, A69, Th16;
then A72: p3 = r1 by A14, A70, Th9;
not q1,p1,p2 is_collinear by A6, Th3;
then q1 = r3 by A10, A71, Th9;
hence r1,r2,r3 is_collinear by A12, A72, Th3; :: 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

A73: now

not p1,p3,q1 is_collinear by A2, A6, A7, Th8;
then A74: not q1,p1,p3 is_collinear by Th3;
A75: not p1,q1,p2 is_collinear by A6, Th3;
assume A76: p1 = q2 ; :: thesis: r1,r2,r3 is_collinear
then p1,q3,q1 is_collinear by A8, Th3;
then p1,q1,r2 is_collinear by A3, A11, A76, Th4;
then A77: q1,p1,r2 is_collinear by Th3;
A78: p1,p3,p2 is_collinear by A7, Th3;
p1,p3,r1 is_collinear by A14, A76, Th3;
then p1,p2,r1 is_collinear by A2, A78, Th4;
then A79: p2,p1,r1 is_collinear by Th3;
q1,p3,r2 is_collinear by A12, Th3;
then A80: q1 = r2 by A77, A74, Th9;
p1,q1,q3 is_collinear by A8, A76, Th3;
then not p1,q3,p2 is_collinear by A3, A76, A75, Th8;
then not p2,p1,q3 is_collinear by Th3;
then r1 = p2 by A13, A79, Th9;
hence r1,r2,r3 is_collinear by A10, A80, Th3; :: thesis: verum

end;

assume A81: p1,p2,q2 is_collinear ; :: thesis: r1,r2,r3 is_collinear

A82: now

assume that
A83: p1 <> q2 and
A84: p3 <> q2 ; :: thesis: r1,r2,r3 is_collinear
p1,q2,p2 is_collinear by A81, Th3;
then p1,p2,r3 is_collinear by A9, A83, Th4;
then A85: p2,p1,r3 is_collinear by Th3;
p1,q2,p3 is_collinear by A7, A15, A81, Th4;
then p3,q2,p1 is_collinear by Th3;
then p3,p1,r1 is_collinear by A14, A84, Th4;
then A86: p1,p3,r1 is_collinear by Th3;
p1,p3,p2 is_collinear by A7, Th3;
then p1,p2,r1 is_collinear by A2, A86, Th4;
then A87: p2,p1,r1 is_collinear by Th3;
not p2,p1,q3 is_collinear by A3, A6, A8, A81, Th14;
then A88: p2 = r1 by A13, A87, Th9;
( not p2,p1,q1 is_collinear & p2,q1,r3 is_collinear ) by A6, A10, Th3;
then p2 = r3 by A85, Th9;
hence r1,r2,r3 is_collinear by A88, ANPROJ_2:def 7; :: thesis: verum

end;

now

assume A89: p3 = q2 ; :: thesis: r1,r2,r3 is_collinear
then q1,q3,p3 is_collinear by A8, Th3;
then A90: not q3,p1,q1 is_collinear by A2, A5, A6, A7, Th13;
p1,p3,p2 is_collinear by A7, Th3;
then p1,p2,r3 is_collinear by A2, A9, A89, Th4;
then A91: p2,p1,r3 is_collinear by Th3;
( not p2,p1,q1 is_collinear & p2,q1,r3 is_collinear ) by A6, A10, Th3;
then A92: p2 = r3 by A91, Th9;
q1,q2,r2 is_collinear by A12, A89, Th3;
then q1,q3,r2 is_collinear by A4, A8, Th4;
then A93: q3,q1,r2 is_collinear by Th3;
q3,p1,r2 is_collinear by A11, Th3;
then r3,r2,r1 is_collinear by A13, A92, A90, A93, Th9;
hence r1,r2,r3 is_collinear by Th3; :: 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