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 A1: ( 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 ) ; :: thesis: r1,r2,r3 is_collinear
then A2: p1 <> p2 by ANPROJ_2:def 7;

A3: now

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

A5: now

assume A6: p3 = q2 ; :: thesis: r1,r2,r3 is_collinear
p1,p3,p2 is_collinear by A1, Th3;
then p1,p2,r3 is_collinear by A1, A6, Th4;
then A7: p2,p1,r3 is_collinear by Th3;
A8: not p2,p1,q1 is_collinear by A1, Th3;
p2,q1,r3 is_collinear by A1, Th3;
then A9: p2 = r3 by A7, A8, Th9;
q1,q3,p3 is_collinear by A1, A6, Th3;
then A10: not q3,p1,q1 is_collinear by A1, Th13;
q1,q2,r2 is_collinear by A1, A6, Th3;
then q1,q3,r2 is_collinear by A1, Th4;
then A11: q3,q1,r2 is_collinear by Th3;
q3,p1,r2 is_collinear by A1, Th3;
then r3,r2,r1 is_collinear by A1, A9, A10, A11, Th9;
hence r1,r2,r3 is_collinear by Th3; :: thesis: verum

end;

A12: now

assume A13: p1 = q2 ; :: thesis: r1,r2,r3 is_collinear
A14: r1 = p2

proof

A15: not p1,q1,p2 is_collinear by A1, Th3;
p1,q1,q3 is_collinear by A1, A13, Th3;
then not p1,q3,p2 is_collinear by A1, A13, A15, Th8;
then A16: not p2,p1,q3 is_collinear by Th3;
( p1,p3,r1 is_collinear & p1,p3,p2 is_collinear ) by A1, A13, Th3;
then p1,p2,r1 is_collinear by A1, Th4;
then p2,p1,r1 is_collinear by Th3;
hence r1 = p2 by A1, A16, Th9; :: thesis: verum

end;

q1 = r2

proof

( p1,q3,q1 is_collinear & p1,q3,r2 is_collinear ) by A1, A13, Th3;
then p1,q1,r2 is_collinear by A1, A13, Th4;
then A17: q1,p1,r2 is_collinear by Th3;
not p1,p3,q1 is_collinear by A1, Th8;
then A18: not q1,p1,p3 is_collinear by Th3;
q1,p3,r2 is_collinear by A1, Th3;
hence q1 = r2 by A17, A18, Th9; :: thesis: verum

end;

hence r1,r2,r3 is_collinear by A1, A14, Th3; :: thesis: verum

end;

now

assume A19: ( p1 <> q2 & p3 <> q2 ) ; :: thesis: r1,r2,r3 is_collinear
( p2 = r1 & p2 = r3 )

proof

thus p2 = r1 :: thesis: p2 = r3

proof

p1,q2,p3 is_collinear by A1, A2, A4, Th4;
then p3,q2,p1 is_collinear by Th3;
then p3,p1,r1 is_collinear by A1, A19, Th4;
then ( p1,p3,r1 is_collinear & p1,p3,p2 is_collinear ) by A1, Th3;
then p1,p2,r1 is_collinear by A1, Th4;
then A20: p2,p1,r1 is_collinear by Th3;
not p2,p1,q3 is_collinear by A1, A4, A19, Th14;
hence p2 = r1 by A1, A20, Th9; :: thesis: verum

end;

thus p2 = r3 :: thesis: verum

proof

p1,q2,p2 is_collinear by A4, Th3;
then p1,p2,r3 is_collinear by A1, A19, Th4;
then A21: p2,p1,r3 is_collinear by Th3;
( not p2,p1,q1 is_collinear & p2,q1,r3 is_collinear ) by A1, Th3;
hence p2 = r3 by A21, Th9; :: thesis: verum

end;

end;

hence r1,r2,r3 is_collinear by ANPROJ_2:def 7; :: thesis: verum

end;

hence r1,r2,r3 is_collinear by A5, A12; :: thesis: verum

end;

now

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

A23: now

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

A25: now

assume A26: p1 = q3 ; :: thesis: r1,r2,r3 is_collinear
( q1 = r3 & p3 = r1 )

proof

thus q1 = r3 :: thesis: p3 = r1

proof

p1,q2,q1 is_collinear by A1, A26, Th3;
then p1,q1,r3 is_collinear by A1, A26, Th4;
then A27: q1,p1,r3 is_collinear by Th3;
not q1,p1,p2 is_collinear by A1, Th3;
hence q1 = r3 by A1, A27, Th9; :: thesis: verum

end;

thus p3 = r1 :: thesis: verum

proof

p1,p2,r1 is_collinear by A1, A26, Th3;
then p1,p3,r1 is_collinear by A1, A2, Th4;
then A28: p3,p1,r1 is_collinear by Th3;
not p3,p1,q2 is_collinear by A1, A26, Th16;
hence p3 = r1 by A1, A28, Th9; :: thesis: verum

end;

end;

hence r1,r2,r3 is_collinear by A1, Th3; :: thesis: verum

end;

A29: now

assume A30: p2 = q3 ; :: thesis: r1,r2,r3 is_collinear
( q2 = r3 & p3 = r2 )

proof

thus q2 = r3 :: thesis: p3 = r2

proof

A31: q2,p1,r3 is_collinear by A1, Th3;
( p2,q1,r3 is_collinear & p2,q1,q2 is_collinear ) by A1, A30, Th3;
then p2,q2,r3 is_collinear by A1, A30, Th4;
then A32: q2,p2,r3 is_collinear by Th3;
not q2,p1,p2 is_collinear

proof

A33: not p2,q1,p1 is_collinear by A1, Th3;
p2,q1,q2 is_collinear by A1, A30, Th3;
then not p2,q2,p1 is_collinear by A1, A30, A33, Th8;
hence not q2,p1,p2 is_collinear by Th3; :: thesis: verum

end;

hence q2 = r3 by A31, A32, Th9; :: thesis: verum

end;

thus p3 = r2 :: thesis: verum

proof

p1,p3,r2 is_collinear by A1, A2, A30, Th4;
then A34: p3,p1,r2 is_collinear by Th3;
not p3,p1,q1 is_collinear

proof

not p1,p3,q1 is_collinear by A1, Th8;
hence not p3,p1,q1 is_collinear by Th3; :: thesis: verum

end;

hence p3 = r2 by A1, A34, Th9; :: thesis: verum

end;

end;

hence r1,r2,r3 is_collinear by A1, Th3; :: thesis: verum

end;

now

assume A35: ( p2 <> q3 & p1 <> q3 ) ; :: thesis: r1,r2,r3 is_collinear
A36: p3 = r1

proof

p2,q3,p1 is_collinear by A24, Th3;
then ( p2,p1,r1 is_collinear & p2,p1,p3 is_collinear ) by A1, A35, Th3, Th4;
then p2,r1,p3 is_collinear by A2, Th4;
then A37: p3,p2,r1 is_collinear by Th3;
not p3,q2,p2 is_collinear

proof

A38: not p2,p1,q2 is_collinear by A22, Th3;
p2,p1,p3 is_collinear by A1, Th3;
then not p2,p3,q2 is_collinear by A1, A38, Th8;
hence not p3,q2,p2 is_collinear by Th3; :: thesis: verum

end;

hence p3 = r1 by A1, A37, Th9; :: thesis: verum

end;

p3 = r2

proof

p1,q3,p2 is_collinear by A24, Th3;
then p1,p2,r2 is_collinear by A1, A35, Th4;
then p1,r2,p3 is_collinear by A1, A2, Th4;
then A39: p3,p1,r2 is_collinear by Th3;
not p1,p3,q1 is_collinear by A1, Th8;
then not p3,q1,p1 is_collinear by Th3;
hence p3 = r2 by A1, A39, Th9; :: thesis: verum

end;

hence r1,r2,r3 is_collinear by A36, ANPROJ_2:def 7; :: thesis: verum

end;

hence r1,r2,r3 is_collinear by A25, A29; :: thesis: verum

end;

now

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

A41: now

assume A42: ( q1,q2,p1 is_collinear or q1,q2,p2 is_collinear or q1,q2,p3 is_collinear ) ; :: thesis: r1,r2,r3 is_collinear

A43: now

assume A44: q1,q2,p1 is_collinear ; :: thesis: r1,r2,r3 is_collinear
( q1 = r2 & q1 = r3 )

proof

thus q1 = r2 :: thesis: q1 = r3

proof

q1,p1,q3 is_collinear by A1, A44, Th4;
then A45: p1,q3,q1 is_collinear by Th3;
p1 <> q3 by A40, ANPROJ_2:def 7;
then p1,r2,q1 is_collinear by A1, A45, Th4;
then A46: q1,p1,r2 is_collinear by Th3;
not p1,p3,q1 is_collinear by A1, Th8;
then ( not q1,p1,p3 is_collinear & q1,p3,r2 is_collinear ) by A1, Th3;
hence q1 = r2 by A46, Th9; :: thesis: verum

end;

thus q1 = r3 :: thesis: verum

proof

A47: p1 <> q2 by A22, ANPROJ_2:def 7;
p1,q2,q1 is_collinear by A44, Th3;
then p1,r3,q1 is_collinear by A1, A47, Th4;
then A48: q1,p1,r3 is_collinear by Th3;
not q1,p2,p1 is_collinear by A1, Th3;
hence q1 = r3 by A1, A48, Th9; :: thesis: verum

end;

end;

hence r1,r2,r3 is_collinear by ANPROJ_2:def 7; :: thesis: verum

end;

A49: now

assume A50: q1,q2,p2 is_collinear ; :: thesis: r1,r2,r3 is_collinear
( q2 = r3 & q2 = r1 )

proof

thus q2 = r3 :: thesis: q2 = r1

proof

A51: p2 <> q1 by A1, ANPROJ_2:def 7;
( p2,q1,r3 is_collinear & p2,q1,q2 is_collinear ) by A1, A50, Th3;
then p2,r3,q2 is_collinear by A51, Th4;
then A52: ( q2,p2,r3 is_collinear & q2,p1,r3 is_collinear ) by A1, Th3;
not q2,p1,p2 is_collinear by A22, Th3;
hence q2 = r3 by A52, Th9; :: thesis: verum

end;

thus q2 = r1 :: thesis: verum

proof

A53: p2 <> q3 by A40, ANPROJ_2:def 7;
( q2,q1,p2 is_collinear & q2,q1,q3 is_collinear ) by A1, A50, Th3;
then q2,p2,q3 is_collinear by A1, Th4;
then p2,q3,q2 is_collinear by Th3;
then p2,r1,q2 is_collinear by A1, A53, Th4;
then A54: ( q2,p2,r1 is_collinear & q2,p3,r1 is_collinear ) by A1, Th3;
( not p2,p1,q2 is_collinear & p2,p1,p3 is_collinear ) by A1, A22, Th3;
then not p2,p3,q2 is_collinear by A1, Th8;
then not q2,p2,p3 is_collinear by Th3;
hence q2 = r1 by A54, Th9; :: thesis: verum

end;

end;

hence r1,r2,r3 is_collinear by ANPROJ_2:def 7; :: thesis: verum

end;

now

assume A55: q1,q2,p3 is_collinear ; :: thesis: r1,r2,r3 is_collinear
( q3 = r2 & q3 = r1 )

proof

thus q3 = r2 :: thesis: q3 = r1

proof

q1,q3,p3 is_collinear by A1, A55, Th4;
then p3,q1,q3 is_collinear by Th3;
then p3,r2,q3 is_collinear by A1, Th4;
then A56: ( q3,p3,r2 is_collinear & q3,p1,r2 is_collinear ) by A1, Th3;
not p1,p3,q3 is_collinear by A1, A40, Th8;
then not q3,p1,p3 is_collinear by Th3;
hence q3 = r2 by A56, Th9; :: thesis: verum

end;

thus q3 = r1 :: thesis: verum

proof

( q2,q1,q3 is_collinear & q2,q1,p3 is_collinear ) by A1, A55, Th3;
then q2,q3,p3 is_collinear by A1, Th4;
then p3,q2,q3 is_collinear by Th3;
then p3,r1,q3 is_collinear by A1, A22, Th4;
then A57: ( q3,p3,r1 is_collinear & q3,p2,r1 is_collinear ) by A1, Th3;
( not p2,p1,q3 is_collinear & p2,p1,p3 is_collinear ) by A1, A40, Th3;
then not p2,p3,q3 is_collinear by A1, Th8;
then not q3,p2,p3 is_collinear by Th3;
hence q3 = r1 by A57, Th9; :: thesis: verum

end;

end;

hence r1,r2,r3 is_collinear by ANPROJ_2:def 7; :: thesis: verum

end;

hence r1,r2,r3 is_collinear by A42, A43, A49; :: thesis: verum

end;

now

assume A58: ( not q1,q2,p1 is_collinear & 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
A59: ( p1,p2,o is_collinear & q1,q2,o is_collinear ) by ANPROJ_2:def 14;
A60: ( o,p1,p3 is_collinear & o,q1,q3 is_collinear & o,p1,p2 is_collinear & o,q1,q2 is_collinear )

proof

p1,p3,o is_collinear by A1, A2, A59, Th4;
hence o,p1,p3 is_collinear by Th3; :: thesis: ( o,q1,q3 is_collinear & o,p1,p2 is_collinear & o,q1,q2 is_collinear )
q1,q3,o is_collinear by A1, A59, Th4;
hence o,q1,q3 is_collinear by Th3; :: thesis: ( o,p1,p2 is_collinear & o,q1,q2 is_collinear )
thus ( o,p1,p2 is_collinear & o,q1,q2 is_collinear ) by A59, Th3; :: thesis: verum

end;

not o,p1,q1 is_collinear

proof

not p1,o,q1 is_collinear by A1, A58, A59, Th8;
hence not o,p1,q1 is_collinear by Th3; :: thesis: verum

end;

hence r1,r2,r3 is_collinear by A1, A2, A22, A40, A58, A59, A60, ANPROJ_2:def 13; :: thesis: verum

end;

hence r1,r2,r3 is_collinear by A41; :: thesis: verum

end;

hence r1,r2,r3 is_collinear by A23; :: thesis: verum

end;

hence r1,r2,r3 is_collinear by A3; :: thesis: verum