let IPP be Desarguesian IncProjSp; for o, b1, a1, b2, a2, b3, a3, r, s, t being POINT of IPP
for C1, C2, C3, A1, A2, A3, B1, B2, B3 being LINE of IPP st {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_distinct & o <> a3 & o <> b1 & o <> b2 & a2 <> b2 holds
ex O being LINE of IPP st {r,s,t} on O
let o, b1, a1, b2, a2, b3, a3, r, s, t be POINT of IPP; for C1, C2, C3, A1, A2, A3, B1, B2, B3 being LINE of IPP st {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_distinct & o <> a3 & o <> b1 & o <> b2 & a2 <> b2 holds
ex O being LINE of IPP st {r,s,t} on O
let C1, C2, C3, A1, A2, A3, B1, B2, B3 be LINE of IPP; ( {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_distinct & o <> a3 & o <> b1 & o <> b2 & a2 <> b2 implies ex O being LINE of IPP st {r,s,t} on O )
assume that
A1:
{o,b1,a1} on C1
and
A2:
{o,a2,b2} on C2
and
A3:
{o,a3,b3} on C3
and
A4:
{a3,a2,t} on A1
and
A5:
{a3,r,a1} on A2
and
A6:
{a2,s,a1} on A3
and
A7:
{t,b2,b3} on B1
and
A8:
{b1,r,b3} on B2
and
A9:
{b1,s,b2} on B3
and
A10:
C1,C2,C3 are_mutually_distinct
and
A11:
o <> a3
and
A12:
o <> b1
and
A13:
o <> b2
and
A14:
a2 <> b2
; ex O being LINE of IPP st {r,s,t} on O
A15:
( r on A2 & r on B2 )
by A5, A8, INCSP_1:2;
A16:
s on B3
by A9, INCSP_1:2;
A17:
a3 on A1
by A4, INCSP_1:2;
A18:
b3 on B1
by A7, INCSP_1:2;
A19:
b2 on B1
by A7, INCSP_1:2;
A20:
b3 on C3
by A3, INCSP_1:2;
A21:
a1 on C1
by A1, INCSP_1:2;
A22:
o on C2
by A2, INCSP_1:2;
A23:
s on A3
by A6, INCSP_1:2;
A24:
a1 on A3
by A6, INCSP_1:2;
A25:
a1 on A2
by A5, INCSP_1:2;
A26:
t on A1
by A4, INCSP_1:2;
A27:
b1 on B2
by A8, INCSP_1:2;
A28:
t on B1
by A7, INCSP_1:2;
A29:
b1 on B3
by A9, INCSP_1:2;
A30:
now ( o <> b3 & o <> a1 & o <> a2 & a1 = b1 implies ex O being LINE of IPP st {r,s,t} on O )assume that
o <> b3
and
o <> a1
and
o <> a2
and A31:
a1 = b1
;
ex O being LINE of IPP st {r,s,t} on OA32:
now ( a3 <> b3 implies ex O being LINE of IPP st {r,s,t} on O )A33:
b3 on B2
by A8, INCSP_1:2;
consider O being
LINE of
IPP such that A34:
(
t on O &
s on O )
by INCPROJ:def 5;
assume A35:
a3 <> b3
;
ex O being LINE of IPP st {r,s,t} on Otake O =
O;
{r,s,t} on OA36:
(
b2 on C2 &
o on C2 )
by A2, INCSP_1:2;
A37:
(
o on C1 &
a2 on C2 )
by A1, A2, INCSP_1:2;
A38:
(
b1 on B3 &
b2 on B3 )
by A9, INCSP_1:2;
A39:
(
b1 on A2 &
a3 on A2 )
by A5, A31, INCSP_1:2;
A40:
(
a3 on C3 &
b3 on C3 )
by A3, INCSP_1:2;
A41:
(
o on C1 &
o on C3 )
by A1, A3, INCSP_1:2;
A42:
a2 on A3
by A6, INCSP_1:2;
(
C1 <> C2 &
b1 on C1 )
by A1, A10, INCSP_1:2, ZFMISC_1:def 5;
then
A3 <> B3
by A12, A14, A37, A36, A38, A42, Th10;
then A43:
b1 = s
by A23, A24, A29, A16, A31, INCPROJ:def 4;
(
C1 <> C3 &
b1 on C1 )
by A1, A10, INCSP_1:2, ZFMISC_1:def 5;
then
A2 <> B2
by A12, A35, A41, A40, A39, A33, Th10;
then
s = r
by A25, A27, A15, A31, A43, INCPROJ:def 4;
hence
{r,s,t} on O
by A34, INCSP_1:2;
verum end; now ( a3 = b3 implies ex B2 being LINE of IPP st {r,s,t} on B2 )A44:
(
a2 on A3 &
b1 on A3 )
by A6, A31, INCSP_1:2;
A45:
(
C2 <> C3 &
o on C2 )
by A2, A10, INCSP_1:2, ZFMISC_1:def 5;
A46:
(
a2 on C2 &
b2 on C2 )
by A2, INCSP_1:2;
A47:
(
o on C1 &
a2 on C2 )
by A1, A2, INCSP_1:2;
A48:
b2 on B3
by A9, INCSP_1:2;
A49:
(
a2 on A1 &
b2 on B1 )
by A4, A7, INCSP_1:2;
A50:
(
o on C3 &
b3 on C3 )
by A3, INCSP_1:2;
assume A51:
a3 = b3
;
ex B2 being LINE of IPP st {r,s,t} on B2then
b3 on A1
by A4, INCSP_1:2;
then
A1 <> B1
by A11, A14, A51, A45, A46, A50, A49, Th10;
then A52:
t = b3
by A17, A26, A28, A18, A51, INCPROJ:def 4;
take B2 =
B2;
{r,s,t} on B2A53:
(
b2 on C2 &
o on C2 )
by A2, INCSP_1:2;
(
C1 <> C2 &
b1 on C1 )
by A1, A10, INCSP_1:2, ZFMISC_1:def 5;
then
A3 <> B3
by A12, A14, A47, A53, A44, A48, Th10;
then
{s,r,t} on B2
by A8, A23, A24, A29, A16, A31, A52, INCPROJ:def 4;
hence
{r,s,t} on B2
by Th11;
verum end; hence
ex
O being
LINE of
IPP st
{r,s,t} on O
by A32;
verum end;
A54:
o on C1
by A1, INCSP_1:2;
A55:
C1 <> C2
by A10, ZFMISC_1:def 5;
A56:
b1 on C1
by A1, INCSP_1:2;
A57:
a2 on A3
by A6, INCSP_1:2;
A58:
b2 on C2
by A2, INCSP_1:2;
A59:
C2 <> C3
by A10, ZFMISC_1:def 5;
A60:
a3 on C3
by A3, INCSP_1:2;
A61:
b3 on B2
by A8, INCSP_1:2;
A62:
a3 on A2
by A5, INCSP_1:2;
A63:
a2 on A1
by A4, INCSP_1:2;
A64:
o on C3
by A3, INCSP_1:2;
A65:
b2 on B3
by A9, INCSP_1:2;
A66:
now ( o <> b3 & o <> a1 & o = a2 implies ex O being LINE of IPP st {r,s,t} on O )assume that A67:
o <> b3
and A68:
o <> a1
and A69:
o = a2
;
ex O being LINE of IPP st {r,s,t} on OA70:
now ( a1 = b1 implies ex O being LINE of IPP st {r,s,t} on O )assume A71:
a1 = b1
;
ex O being LINE of IPP st {r,s,t} on OA72:
now ( a3 = b3 implies ex B2 being LINE of IPP st {r,s,t} on B2 )A73:
(
a2 on A1 &
b2 on B1 )
by A4, A7, INCSP_1:2;
A74:
(
b2 on C2 &
b3 on C3 )
by A2, A3, INCSP_1:2;
A75:
(
b2 on C2 &
a2 on A3 )
by A2, A6, INCSP_1:2;
A76:
(
o on C2 &
b1 on C1 )
by A1, A2, INCSP_1:2;
A77:
(
C1 <> C2 &
o on C1 )
by A1, A10, INCSP_1:2, ZFMISC_1:def 5;
assume A78:
a3 = b3
;
ex B2 being LINE of IPP st {r,s,t} on B2take B2 =
B2;
{r,s,t} on B2A79:
b2 on B3
by A9, INCSP_1:2;
(
b1 on A3 &
a2 on C2 )
by A2, A6, A71, INCSP_1:2;
then
A3 <> B3
by A12, A14, A77, A76, A75, A79, Th10;
then A80:
s = b1
by A23, A24, A29, A16, A71, INCPROJ:def 4;
A81:
(
o on C3 &
a2 on C2 )
by A2, A3, INCSP_1:2;
A82:
(
C2 <> C3 &
o on C2 )
by A2, A10, INCSP_1:2, ZFMISC_1:def 5;
b3 on A1
by A4, A78, INCSP_1:2;
then
A1 <> B1
by A11, A14, A78, A82, A81, A74, A73, Th10;
then
{s,r,t} on B2
by A8, A17, A26, A28, A18, A78, A80, INCPROJ:def 4;
hence
{r,s,t} on B2
by Th11;
verum end; now ( a3 <> b3 implies ex O being LINE of IPP st {r,s,t} on O )A83:
(
o on C3 &
a1 on C1 )
by A1, A3, INCSP_1:2;
A84:
(
a1 on A2 &
a3 on A2 )
by A5, INCSP_1:2;
A85:
b3 on B2
by A8, INCSP_1:2;
consider O being
LINE of
IPP such that A86:
(
t on O &
s on O )
by INCPROJ:def 5;
assume A87:
a3 <> b3
;
ex O being LINE of IPP st {r,s,t} on Otake O =
O;
{r,s,t} on OA88:
(
a3 on C3 &
b3 on C3 )
by A3, INCSP_1:2;
(
C1 <> C3 &
o on C1 )
by A1, A10, INCSP_1:2, ZFMISC_1:def 5;
then
A2 <> B2
by A12, A71, A87, A83, A88, A84, A85, Th10;
then A89:
r = b1
by A25, A27, A15, A71, INCPROJ:def 4;
(
A3 = C1 &
B3 <> C1 )
by A13, A54, A21, A22, A58, A57, A24, A65, A55, A68, A69, INCPROJ:def 4;
then
r = s
by A23, A24, A29, A16, A71, A89, INCPROJ:def 4;
hence
{r,s,t} on O
by A86, INCSP_1:2;
verum end; hence
ex
O being
LINE of
IPP st
{r,s,t} on O
by A72;
verum end; now ( a1 <> b1 implies ex O being LINE of IPP st {r,s,t} on O )assume A90:
a1 <> b1
;
ex O being LINE of IPP st {r,s,t} on OA91:
now ( a3 = b3 implies ex O being Element of the Lines of IPP st {r,s,t} on O )A92:
B1 <> C3
by A13, A22, A58, A64, A19, A59, INCPROJ:def 4;
A93:
(
o on C3 &
a1 on C1 )
by A1, A3, INCSP_1:2;
consider O being
Element of the
Lines of
IPP such that A94:
(
t on O &
s on O )
by INCPROJ:def 5;
A95:
(
C1 <> C3 &
o on C1 )
by A1, A10, INCSP_1:2, ZFMISC_1:def 5;
A96:
(
a1 on A2 &
b1 on B2 )
by A5, A8, INCSP_1:2;
A97:
(
b1 on C1 &
b3 on C3 )
by A1, A3, INCSP_1:2;
assume A98:
a3 = b3
;
ex O being Element of the Lines of IPP st {r,s,t} on Othen
b3 on A2
by A5, INCSP_1:2;
then
A2 <> B2
by A11, A90, A98, A95, A93, A97, A96, Th10;
then A99:
r = b3
by A62, A15, A61, A98, INCPROJ:def 4;
take O =
O;
{r,s,t} on O
A1 = C3
by A64, A60, A17, A63, A67, A69, A98, INCPROJ:def 4;
then
r = t
by A20, A26, A28, A18, A92, A99, INCPROJ:def 4;
hence
{r,s,t} on O
by A94, INCSP_1:2;
verum end; now ( a3 <> b3 implies ex B2 being LINE of IPP st {r,s,t} on B2 )assume
a3 <> b3
;
ex B2 being LINE of IPP st {r,s,t} on B2take B2 =
B2;
{r,s,t} on B2
(
A3 = C1 &
B3 <> C1 )
by A13, A54, A21, A22, A58, A57, A24, A65, A55, A68, A69, INCPROJ:def 4;
then A100:
b1 = s
by A56, A23, A29, A16, INCPROJ:def 4;
(
A1 = C3 &
B1 <> C3 )
by A11, A13, A22, A58, A64, A60, A17, A63, A19, A59, A69, INCPROJ:def 4;
then
{s,r,t} on B2
by A8, A20, A26, A28, A18, A100, INCPROJ:def 4;
hence
{r,s,t} on B2
by Th11;
verum end; hence
ex
O being
LINE of
IPP st
{r,s,t} on O
by A91;
verum end; hence
ex
O being
LINE of
IPP st
{r,s,t} on O
by A70;
verum end;
A101:
C3 <> C1
by A10, ZFMISC_1:def 5;
A102:
a2 on C2
by A2, INCSP_1:2;
A103:
now ( o <> b3 & o = a1 implies ex O being LINE of IPP st {r,s,t} on O )assume that A104:
o <> b3
and A105:
o = a1
;
ex O being LINE of IPP st {r,s,t} on OA106:
now ( o <> a2 implies ex O being LINE of IPP st {r,s,t} on O )A107:
now ( a3 = b3 implies ex O being LINE of IPP st {r,s,t} on O )A108:
B2 <> C3
by A12, A54, A56, A64, A27, A101, INCPROJ:def 4;
assume A109:
a3 = b3
;
ex O being LINE of IPP st {r,s,t} on Othen
A2 = C3
by A64, A60, A62, A25, A104, A105, INCPROJ:def 4;
then A110:
r = b3
by A20, A15, A61, A108, INCPROJ:def 4;
A111:
(
b2 on C2 &
b3 on C3 )
by A2, A3, INCSP_1:2;
A112:
(
o on C3 &
a2 on C2 )
by A2, A3, INCSP_1:2;
A113:
(
a2 on A1 &
b2 on B1 )
by A4, A7, INCSP_1:2;
consider O being
LINE of
IPP such that A114:
(
t on O &
s on O )
by INCPROJ:def 5;
A115:
(
C2 <> C3 &
o on C2 )
by A2, A10, INCSP_1:2, ZFMISC_1:def 5;
take O =
O;
{r,s,t} on O
b3 on A1
by A4, A109, INCSP_1:2;
then
A1 <> B1
by A11, A14, A109, A115, A112, A111, A113, Th10;
then
r = t
by A17, A26, A28, A18, A109, A110, INCPROJ:def 4;
hence
{r,s,t} on O
by A114, INCSP_1:2;
verum end; assume A116:
o <> a2
;
ex O being LINE of IPP st {r,s,t} on Onow ( a3 <> b3 implies ex B1 being LINE of IPP st {r,s,t} on B1 )assume
a3 <> b3
;
ex B1 being LINE of IPP st {r,s,t} on B1take B1 =
B1;
{r,s,t} on B1
(
A3 = C2 &
B3 <> C2 )
by A12, A54, A56, A22, A102, A57, A24, A29, A55, A105, A116, INCPROJ:def 4;
then A117:
s = b2
by A58, A23, A16, A65, INCPROJ:def 4;
(
A2 = C3 &
B2 <> C3 )
by A11, A12, A54, A56, A64, A60, A62, A25, A27, A101, A105, INCPROJ:def 4;
then
{t,s,r} on B1
by A7, A20, A15, A61, A117, INCPROJ:def 4;
hence
{r,s,t} on B1
by Th11;
verum end; hence
ex
O being
LINE of
IPP st
{r,s,t} on O
by A107;
verum now ( o = a2 implies ex O being LINE of IPP st {r,s,t} on O )assume
o = a2
;
ex O being LINE of IPP st {r,s,t} on Othen A118:
A1 = C3
by A11, A64, A60, A17, A63, INCPROJ:def 4;
(
A2 = C3 &
B2 <> C3 )
by A11, A12, A54, A56, A64, A60, A62, A25, A27, A101, A105, INCPROJ:def 4;
then A119:
r = b3
by A20, A15, A61, INCPROJ:def 4;
consider O being
LINE of
IPP such that A120:
(
t on O &
s on O )
by INCPROJ:def 5;
take O =
O;
{r,s,t} on O
B1 <> C3
by A13, A22, A58, A64, A19, A59, INCPROJ:def 4;
then
r = t
by A20, A26, A28, A18, A118, A119, INCPROJ:def 4;
hence
{r,s,t} on O
by A120, INCSP_1:2;
verum end; hence
ex
O being
LINE of
IPP st
{r,s,t} on O
by A106;
verum end;
A121:
C1 <> B3
by A13, A54, A22, A58, A65, A55, INCPROJ:def 4;
A122:
now ( o = b3 implies ex O being LINE of IPP st {r,s,t} on O )assume A123:
o = b3
;
ex O being LINE of IPP st {r,s,t} on OA124:
now ( a1 = o implies ex O being LINE of IPP st {r,s,t} on O )assume A125:
a1 = o
;
ex O being LINE of IPP st {r,s,t} on OA126:
now ( o = a2 implies ex O being LINE of IPP st {r,s,t} on O )assume
o = a2
;
ex O being LINE of IPP st {r,s,t} on Othen A127:
A1 = C3
by A11, A64, A60, A17, A63, INCPROJ:def 4;
(
A2 = C3 &
B2 = C1 )
by A11, A12, A54, A56, A64, A60, A62, A25, A27, A61, A123, A125, INCPROJ:def 4;
then A128:
o = r
by A54, A64, A15, A101, INCPROJ:def 4;
consider O being
LINE of
IPP such that A129:
(
t on O &
s on O )
by INCPROJ:def 5;
take O =
O;
{r,s,t} on O
B1 = C2
by A13, A22, A58, A19, A18, A123, INCPROJ:def 4;
then
r = t
by A22, A64, A26, A28, A59, A128, A127, INCPROJ:def 4;
hence
{r,s,t} on O
by A129, INCSP_1:2;
verum end; now ( o <> a2 implies ex C2 being LINE of IPP st {r,s,t} on C2 )
(
B2 = C1 &
A2 = C3 )
by A11, A12, A54, A56, A64, A60, A62, A25, A27, A61, A123, A125, INCPROJ:def 4;
then A130:
r = o
by A54, A64, A15, A101, INCPROJ:def 4;
assume
o <> a2
;
ex C2 being LINE of IPP st {r,s,t} on C2then A131:
C2 = A3
by A22, A102, A57, A24, A125, INCPROJ:def 4;
take C2 =
C2;
{r,s,t} on C2
C2 = B1
by A13, A22, A58, A19, A18, A123, INCPROJ:def 4;
hence
{r,s,t} on C2
by A22, A23, A28, A131, A130, INCSP_1:2;
verum hence
ex
O being
LINE of
IPP st
{r,s,t} on O
by A126;
verum end; now ( a1 <> o implies ex O being LINE of IPP st {r,s,t} on O )assume A132:
a1 <> o
;
ex O being LINE of IPP st {r,s,t} on OA133:
now ( o = a2 implies ex B2 being LINE of IPP st {r,s,t} on B2 )assume A134:
o = a2
;
ex B2 being LINE of IPP st {r,s,t} on B2then A135:
A1 = C3
by A11, A64, A60, A17, A63, INCPROJ:def 4;
take B2 =
B2;
{r,s,t} on B2
C1 = A3
by A54, A21, A57, A24, A132, A134, INCPROJ:def 4;
then A136:
b1 = s
by A56, A23, A29, A16, A121, INCPROJ:def 4;
B1 = C2
by A13, A22, A58, A19, A18, A123, INCPROJ:def 4;
then
{s,r,t} on B2
by A8, A20, A26, A28, A18, A59, A136, A135, INCPROJ:def 4;
hence
{r,s,t} on B2
by Th11;
verum end; now ( o <> a2 implies ex A3 being LINE of IPP st {r,s,t} on A3 )assume
o <> a2
;
ex A3 being LINE of IPP st {r,s,t} on A3take A3 =
A3;
{r,s,t} on A3
(
B2 = C1 &
A2 <> C1 )
by A11, A12, A54, A56, A64, A60, A62, A27, A61, A101, A123, INCPROJ:def 4;
then A137:
r = a1
by A21, A25, A15, INCPROJ:def 4;
(
B1 = C2 &
A1 <> C2 )
by A11, A13, A22, A58, A64, A60, A17, A19, A18, A59, A123, INCPROJ:def 4;
then
{t,s,r} on A3
by A6, A102, A63, A26, A28, A137, INCPROJ:def 4;
hence
{r,s,t} on A3
by Th11;
verum end; hence
ex
O being
LINE of
IPP st
{r,s,t} on O
by A133;
verum end; hence
ex
O being
LINE of
IPP st
{r,s,t} on O
by A124;
verum end;
now ( o <> b3 & o <> a1 & o <> a2 & a1 <> b1 & a3 = b3 implies ex O being Element of the Lines of IPP st {r,s,t} on O )A138:
(
b2 on B1 &
a2 on C2 )
by A2, A7, INCSP_1:2;
A139:
(
o on C3 &
b3 on C3 )
by A3, INCSP_1:2;
A140:
(
a1 on A2 &
b1 on B2 )
by A5, A8, INCSP_1:2;
A141:
(
b2 on C2 &
o on C2 )
by A2, INCSP_1:2;
A142:
(
b3 on B1 &
t on A1 )
by A4, A7, INCSP_1:2;
A143:
t on B1
by A7, INCSP_1:2;
consider O being
Element of the
Lines of
IPP such that A144:
(
t on O &
s on O )
by INCPROJ:def 5;
assume that A145:
o <> b3
and
o <> a1
and
o <> a2
and A146:
a1 <> b1
and A147:
a3 = b3
;
ex O being Element of the Lines of IPP st {r,s,t} on Otake O =
O;
{r,s,t} on OA148:
C1 <> C3
by A10, ZFMISC_1:def 5;
b3 on A2
by A5, A147, INCSP_1:2;
then
A2 <> B2
by A54, A56, A21, A64, A20, A145, A146, A140, A148, Th10;
then A149:
b3 = r
by A62, A15, A61, A147, INCPROJ:def 4;
A150:
b3 on A1
by A4, A147, INCSP_1:2;
(
C2 <> C3 &
a2 on A1 )
by A4, A10, INCSP_1:2, ZFMISC_1:def 5;
then
A1 <> B1
by A14, A145, A150, A138, A141, A139, Th10;
then
r = t
by A150, A142, A143, A149, INCPROJ:def 4;
hence
{r,s,t} on O
by A144, INCSP_1:2;
verum end;
hence
ex O being LINE of IPP st {r,s,t} on O
by A1, A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, A12, A13, A14, A122, A103, A66, A30, INCPROJ:def 13; verum