let IPP be Desarguesian IncProjSp; :: thesis:
let o, b1, a1, b2, a2, b3, a3, r, s, t be POINT of IPP; :: thesis:
let C1, C2, C3, A1, A2, A3, B1, B2, B3 be LINE of IPP; :: thesis:
assume A1: ( {o,b1,a1} on C1 & {o,a2,b2} on C2 & {o,a3,b3} on C3 & {a3,a2,t} on A1 & {a3,r,a1} on A2 & {a2,s,a1} on A3 & {t,b2,b3} on B1 & {b1,r,b3} on B2 & {b1,s,b2} on B3 & C1,C2,C3 are_mutually_different & o <> a3 & o <> b1 & o <> b2 & a2 <> b2 ) ; :: thesis:
then A2: ( o on C1 & b1 on C1 & a1 on C1 & o on C2 & a2 on C2 & b2 on C2 & o on C3 & a3 on C3 & b3 on C3 ) by INCSP_1:12;
A3: ( a3 on A1 & a2 on A1 & t on A1 & a3 on A2 & r on A2 & a1 on A2 & a2 on A3 & s on A3 & a1 on A3 ) by A1, INCSP_1:12;
A4: ( t on B1 & b2 on B1 & b3 on B1 & b1 on B2 & r on B2 & b3 on B2 & b1 on B3 & s on B3 & b2 on B3 ) by A1, INCSP_1:12;
A5: ( C1 <> C2 & C2 <> C3 & C3 <> C1 ) by A1, ZFMISC_1:def 5;
then A6: ( C1 <> B3 & C2 <> B3 ) by A1, A2, A4, INCPROJ:def 9;

A7: now

assume A8: o = b3 ; :: thesis:

A9: now

assume A10: a1 = o ; :: thesis:

A11: now

assume A12: o = a2 ; :: thesis:
A13: A2 = C3 by A1, A2, A3, A10, INCPROJ:def 9;
B2 = C1 by A1, A2, A4, A8, INCPROJ:def 9;
then A14: o = r by A2, A3, A4, A5, A13, INCPROJ:def 9;
A15: A1 = C3 by A1, A2, A3, A12, INCPROJ:def 9;
B1 = C2 by A1, A2, A4, A8, INCPROJ:def 9;
then A16: r = t by A2, A3, A4, A5, A14, A15, INCPROJ:def 9;
consider O being LINE of IPP such that
A17: ( t on O & s on O ) by INCPROJ:def 10;
take O = O; :: thesis:
thus {r,s,t} on O by A16, A17, INCSP_1:12; :: thesis:

end;

now

assume A18: o <> a2 ; :: thesis:
A19: C2 = B1 by A1, A2, A4, A8, INCPROJ:def 9;
A20: C2 = A3 by A2, A3, A10, A18, INCPROJ:def 9;
A21: B2 = C1 by A1, A2, A4, A8, INCPROJ:def 9;
A2 = C3 by A1, A2, A3, A10, INCPROJ:def 9;
then A22: r = o by A2, A3, A4, A5, A21, INCPROJ:def 9;
take C2 = C2; :: thesis:
thus {r,s,t} on C2 by A2, A3, A4, A19, A20, A22, INCSP_1:12; :: thesis:

end;

hence ex O being LINE of IPP st {r,s,t} on O by A11; :: thesis:

end;

now

assume A23: a1 <> o ; :: thesis:

now

A24: now

assume A25: o = a2 ; :: thesis:
then C1 = A3 by A2, A3, A23, INCPROJ:def 9;
then A26: b1 = s by A2, A3, A4, A6, INCPROJ:def 9;
A27: B1 = C2 by A1, A2, A4, A8, INCPROJ:def 9;
A1 = C3 by A1, A2, A3, A25, INCPROJ:def 9;
then A28: {s,r,t} on B2 by A1, A2, A3, A4, A5, A26, A27, INCPROJ:def 9;
take B2 = B2; :: thesis:
thus {r,s,t} on B2 by A28, Th13; :: thesis:

end;

now

assume o <> a2 ; :: thesis:
A29: B2 = C1 by A1, A2, A4, A8, INCPROJ:def 9;
A30: B1 = C2 by A1, A2, A4, A8, INCPROJ:def 9;
A31: A2 <> C1 by A1, A2, A3, A5, INCPROJ:def 9;
A32: A1 <> C2 by A1, A2, A3, A5, INCPROJ:def 9;
r = a1 by A2, A3, A4, A29, A31, INCPROJ:def 9;
then A33: {t,s,r} on A3 by A1, A2, A3, A4, A30, A32, INCPROJ:def 9;
take A3 = A3; :: thesis:
thus {r,s,t} on A3 by A33, Th13; :: thesis:

end;

hence ex O being LINE of IPP st {r,s,t} on O by A24; :: thesis:

end;

hence ex O being LINE of IPP st {r,s,t} on O ; :: thesis:

end;

hence ex O being LINE of IPP st {r,s,t} on O by A9; :: thesis:

end;

A34: now

assume A35: ( o <> b3 & o = a1 ) ; :: thesis:

A36: now

assume o = a2 ; :: thesis:
then A37: A1 = C3 by A1, A2, A3, INCPROJ:def 9;
A38: A2 = C3 by A1, A2, A3, A35, INCPROJ:def 9;
A39: B2 <> C3 by A1, A2, A4, A5, INCPROJ:def 9;
A40: B1 <> C3 by A1, A2, A4, A5, INCPROJ:def 9;
r = b3 by A2, A3, A4, A38, A39, INCPROJ:def 9;
then A41: r = t by A2, A3, A4, A37, A40, INCPROJ:def 9;
consider O being LINE of IPP such that
A42: ( t on O & s on O ) by INCPROJ:def 10;
take O = O; :: thesis:
thus {r,s,t} on O by A41, A42, INCSP_1:12; :: thesis:

end;

now

assume A43: o <> a2 ; :: thesis:

A44: now

assume A45: a3 = b3 ; :: thesis:
A46: A1 <> B1

proof

( C2 <> C3 & a2 <> b2 & b3 <> o & o on C2 & o on C3 & a2 on C2 & b2 on C2 & b3 on C3 & a2 on A1 & b3 on A1 & b2 on B1 & b3 on B1 ) by A1, A45, INCSP_1:12, ZFMISC_1:def 5;
hence A1 <> B1 by Th12; :: thesis:

end;

A47: B2 <> C3 by A1, A2, A4, A5, INCPROJ:def 9;
A2 = C3 by A2, A3, A35, A45, INCPROJ:def 9;
then r = b3 by A2, A3, A4, A47, INCPROJ:def 9;
then A48: r = t by A3, A4, A45, A46, INCPROJ:def 9;
consider O being LINE of IPP such that
A49: ( t on O & s on O ) by INCPROJ:def 10;
take O = O; :: thesis:
thus {r,s,t} on O by A48, A49, INCSP_1:12; :: thesis:

end;

now

assume a3 <> b3 ; :: thesis:
A50: A3 = C2 by A2, A3, A35, A43, INCPROJ:def 9;
A51: A2 = C3 by A1, A2, A3, A35, INCPROJ:def 9;
A52: B3 <> C2 by A1, A2, A4, A5, INCPROJ:def 9;
A53: B2 <> C3 by A1, A2, A4, A5, INCPROJ:def 9;
s = b2 by A2, A3, A4, A50, A52, INCPROJ:def 9;
then A54: {t,s,r} on B1 by A1, A2, A3, A4, A51, A53, INCPROJ:def 9;
take B1 = B1; :: thesis:
thus {r,s,t} on B1 by A54, Th13; :: thesis:

end;

hence ex O being LINE of IPP st {r,s,t} on O by A44; :: thesis:

end;

hence ex O being LINE of IPP st {r,s,t} on O by A36; :: thesis:

end;

A55: now

assume A56: ( o <> b3 & o <> a1 & o = a2 ) ; :: thesis:

A57: now

assume A58: a1 = b1 ; :: thesis:

A59: now

assume A60: a3 = b3 ; :: thesis:
A61: A3 <> B3

proof

( C1 <> C2 & o <> b1 & a2 <> b2 & o on C1 & o on C2 & b1 on C1 & b1 on A3 & a2 on C2 & b2 on C2 & a2 on A3 & b2 on B3 ) by A1, A58, INCSP_1:12, ZFMISC_1:def 5;
hence A3 <> B3 by Th12; :: thesis:

end;

A62: A1 <> B1

proof

( C2 <> C3 & a2 <> b2 & o <> b3 & o on C2 & o on C3 & a2 on C2 & b2 on C2 & b3 on C3 & a2 on A1 & b3 on A1 & b2 on B1 & b3 on B1 ) by A1, A60, INCSP_1:12, ZFMISC_1:def 5;
hence A1 <> B1 by Th12; :: thesis:

end;

s = b1 by A3, A4, A58, A61, INCPROJ:def 9;
then A63: {s,r,t} on B2 by A1, A3, A4, A60, A62, INCPROJ:def 9;
take B2 = B2; :: thesis:
thus {r,s,t} on B2 by A63, Th13; :: thesis:

end;

now

assume A64: a3 <> b3 ; :: thesis:
A65: A3 = C1 by A2, A3, A56, INCPROJ:def 9;
A66: A2 <> B2

proof

( C1 <> C3 & o <> a1 & a3 <> b3 & o on C1 & o on C3 & a1 on C1 & a3 on C3 & b3 on C3 & a1 on A2 & a3 on A2 & a1 on B2 & b3 on B2 ) by A1, A58, A64, INCSP_1:12, ZFMISC_1:def 5;
hence A2 <> B2 by Th12; :: thesis:

end;

A67: B3 <> C1 by A1, A2, A4, A5, INCPROJ:def 9;
r = b1 by A3, A4, A58, A66, INCPROJ:def 9;
then A68: r = s by A3, A4, A58, A65, A67, INCPROJ:def 9;
consider O being LINE of IPP such that
A69: ( t on O & s on O ) by INCPROJ:def 10;
take O = O; :: thesis:
thus {r,s,t} on O by A68, A69, INCSP_1:12; :: thesis:

end;

hence ex O being LINE of IPP st {r,s,t} on O by A59; :: thesis:

end;

now

assume A70: a1 <> b1 ; :: thesis:

A71: now

assume A72: a3 = b3 ; :: thesis:
then A73: A1 = C3 by A2, A3, A56, INCPROJ:def 9;
A74: A2 <> B2

proof

( C1 <> C3 & a1 <> b1 & o <> b3 & o on C1 & o on C3 & a1 on C1 & b1 on C1 & b3 on C3 & a1 on A2 & b3 on A2 & b1 on B2 & b3 on B2 ) by A1, A70, A72, INCSP_1:12, ZFMISC_1:def 5;
hence A2 <> B2 by Th12; :: thesis:

end;

A75: B1 <> C3 by A1, A2, A4, A5, INCPROJ:def 9;
r = b3 by A3, A4, A72, A74, INCPROJ:def 9;
then A76: r = t by A2, A3, A4, A73, A75, INCPROJ:def 9;
consider O being Element of the Lines of IPP such that
A77: ( t on O & s on O ) by INCPROJ:def 10;
take O = O; :: thesis:
thus {r,s,t} on O by A76, A77, INCSP_1:12; :: thesis:

end;

now

assume a3 <> b3 ; :: thesis:
A78: A3 = C1 by A2, A3, A56, INCPROJ:def 9;
A79: A1 = C3 by A1, A2, A3, A56, INCPROJ:def 9;
A80: B3 <> C1 by A1, A2, A4, A5, INCPROJ:def 9;
A81: B1 <> C3 by A1, A2, A4, A5, INCPROJ:def 9;
b1 = s by A2, A3, A4, A78, A80, INCPROJ:def 9;
then A82: {s,r,t} on B2 by A1, A2, A3, A4, A79, A81, INCPROJ:def 9;
take B2 = B2; :: thesis:
thus {r,s,t} on B2 by A82, Th13; :: thesis:

end;

hence ex O being LINE of IPP st {r,s,t} on O by A71; :: thesis:

end;

hence ex O being LINE of IPP st {r,s,t} on O by A57; :: thesis:

end;

A83: now

assume A84: ( o <> b3 & o <> a1 & o <> a2 & a1 = b1 ) ; :: thesis:

A85: now

assume A86: a3 = b3 ; :: thesis:
then ( a2 <> b2 & C2 <> C3 & o <> b3 & o on C2 & a2 on C2 & b2 on C2 & o on C3 & b3 on C3 & a2 on A1 & b3 on A1 & b2 on B1 & b3 on B1 ) by A1, INCSP_1:12, ZFMISC_1:def 5;
then A87: A1 <> B1 by Th12;
( b1 <> o & a2 <> b2 & C1 <> C2 & b1 on C1 & o on C1 & a2 on C2 & b2 on C2 & o on C2 & a2 on A3 & b1 on A3 & b1 on B3 & b2 on B3 ) by A1, A84, INCSP_1:12, ZFMISC_1:def 5;
then A88: A3 <> B3 by Th12;
t = b3 by A3, A4, A86, A87, INCPROJ:def 9;
then A89: {s,r,t} on B2 by A1, A3, A4, A84, A88, INCPROJ:def 9;
take B2 = B2; :: thesis:
thus {r,s,t} on B2 by A89, Th13; :: thesis:

end;

now

assume A90: a3 <> b3 ; :: thesis:
( C1 <> C2 & o <> b1 & a2 <> b2 & a1 on C1 & b1 on C1 & o on C1 & a2 on C2 & b2 on C2 & o on C2 & b1 on B3 & b2 on B3 & b1 on A3 & a2 on A3 ) by A1, A84, INCSP_1:12, ZFMISC_1:def 5;
then A3 <> B3 by Th12;
then A91: b1 = s by A3, A4, A84, INCPROJ:def 9;
( a3 <> b3 & b1 <> o & C1 <> C3 & b1 on C1 & o on C1 & o on C3 & a3 on C3 & b3 on C3 & b1 on A2 & a3 on A2 & b1 on B2 & b3 on B2 ) by A1, A84, A90, INCSP_1:12, ZFMISC_1:def 5;
then A2 <> B2 by Th12;
then A92: s = r by A3, A4, A84, A91, INCPROJ:def 9;
consider O being LINE of IPP such that
A93: ( t on O & s on O ) by INCPROJ:def 10;
take O = O; :: thesis:
thus {r,s,t} on O by A92, A93, INCSP_1:12; :: thesis:

end;

hence ex O being LINE of IPP st {r,s,t} on O by A85; :: thesis:

end;

now

assume A94: ( o <> b3 & o <> a1 & o <> a2 & a1 <> b1 & a3 = b3 ) ; :: thesis:
then A95: ( b3 on A2 & a1 on A2 & b3 on B2 & b1 on B2 & a1 <> b1 & C1 <> C3 & o <> b3 & r on A2 & r on B2 ) by A1, INCSP_1:12, ZFMISC_1:def 5;
A96: ( C2 <> C3 & b3 on A1 & a2 on A1 & b2 on B1 & b3 on B1 & a2 <> b2 & o <> b3 & a2 on C2 & b2 on C2 & o on C2 & o on C3 & b3 on C3 & t on A1 & t on B1 ) by A1, A94, INCSP_1:12, ZFMISC_1:def 5;
A97: A2 <> B2 by A2, A95, Th12;
A98: A1 <> B1 by A96, Th12;
b3 = r by A3, A4, A94, A97, INCPROJ:def 9;
then A99: r = t by A96, A98, INCPROJ:def 9;
consider O being Element of the Lines of IPP such that
A100: ( t on O & s on O ) by INCPROJ:def 10;
take O = O; :: thesis:
thus {r,s,t} on O by A99, A100, INCSP_1:12; :: thesis:

end;

hence ex O being LINE of IPP st {r,s,t} on O by A1, A7, A34, A55, A83, INCPROJ:def 19; :: thesis: