let IPP be 2-dimensional Desarguesian IncProjSp; for a, b, c, p, d, q, pp9 being POINT of IPP
for A, C, Q, B, O, O1, O2, O3 being LINE of IPP st not a on A & not a on C & not b on C & not b on Q & not A,B,C are_concurrent & not B,C,O are_concurrent & A <> Q & Q <> C & a <> b & {c,p} on A & d on B & {c,d} on C & {a,b,q} on O & {c,pp9} on Q & {a,d,p} on O1 & {q,p,pp9} on O2 & {b,d,pp9} on O3 holds
( q <> a & q <> b & not q on A & not q on Q )
let a, b, c, p, d, q, pp9 be POINT of IPP; for A, C, Q, B, O, O1, O2, O3 being LINE of IPP st not a on A & not a on C & not b on C & not b on Q & not A,B,C are_concurrent & not B,C,O are_concurrent & A <> Q & Q <> C & a <> b & {c,p} on A & d on B & {c,d} on C & {a,b,q} on O & {c,pp9} on Q & {a,d,p} on O1 & {q,p,pp9} on O2 & {b,d,pp9} on O3 holds
( q <> a & q <> b & not q on A & not q on Q )
let A, C, Q, B, O, O1, O2, O3 be LINE of IPP; ( not a on A & not a on C & not b on C & not b on Q & not A,B,C are_concurrent & not B,C,O are_concurrent & A <> Q & Q <> C & a <> b & {c,p} on A & d on B & {c,d} on C & {a,b,q} on O & {c,pp9} on Q & {a,d,p} on O1 & {q,p,pp9} on O2 & {b,d,pp9} on O3 implies ( q <> a & q <> b & not q on A & not q on Q ) )
assume that
A1:
not a on A
and
A2:
not a on C
and
A3:
not b on C
and
A4:
not b on Q
and
A5:
not A,B,C are_concurrent
and
A6:
not B,C,O are_concurrent
and
A7:
A <> Q
and
A8:
Q <> C
and
A9:
a <> b
and
A10:
{c,p} on A
and
A11:
d on B
and
A12:
{c,d} on C
and
A13:
{a,b,q} on O
and
A14:
{c,pp9} on Q
and
A15:
{a,d,p} on O1
and
A16:
{q,p,pp9} on O2
and
A17:
{b,d,pp9} on O3
; ( q <> a & q <> b & not q on A & not q on Q )
A18:
d on C
by A12, INCSP_1:11;
A19:
c on C
by A12, INCSP_1:11;
A20:
c on A
by A10, INCSP_1:11;
then A21:
c <> d
by A5, A11, A19, Def1;
A22:
d on O1
by A15, INCSP_1:12;
A23:
pp9 on Q
by A14, INCSP_1:11;
A24:
pp9 on O3
by A17, INCSP_1:12;
A25:
pp9 on O2
by A16, INCSP_1:12;
A26:
a on O1
by A15, INCSP_1:12;
A27:
b on O3
by A17, INCSP_1:12;
A28:
d on O3
by A17, INCSP_1:12;
A29:
q on O
by A13, INCSP_1:12;
A30:
b on O
by A13, INCSP_1:12;
A31:
q <> pp9
proof
assume
not
q <> pp9
;
contradiction
then
O3 = O
by A4, A30, A29, A27, A24, A23, INCPROJ:def 9;
hence
contradiction
by A6, A11, A18, A28, Def1;
verum
end;
A32:
( pp9 on O2 & q on O2 )
by A16, INCSP_1:12;
A33:
( pp9 on Q & p on O2 )
by A14, A16, INCSP_1:11, INCSP_1:12;
A34:
p on A
by A10, INCSP_1:11;
A35:
c on Q
by A14, INCSP_1:11;
then A36:
pp9 <> d
by A8, A19, A18, A23, A21, INCPROJ:def 9;
A37:
O1 <> O2
proof
assume
not
O1 <> O2
;
contradiction
then A38:
a on O3
by A26, A22, A25, A28, A24, A36, INCPROJ:def 9;
(
a on O &
b on O )
by A13, INCSP_1:12;
then
d on O
by A9, A28, A27, A38, INCPROJ:def 9;
hence
contradiction
by A6, A11, A18, Def1;
verum
end;
A39:
p on O1
by A15, INCSP_1:12;
then A40:
p <> c
by A2, A19, A18, A26, A22, A21, INCPROJ:def 9;
A41:
not q on Q
A42:
a on O
by A13, INCSP_1:12;
A43:
q <> p
proof
assume
not
q <> p
;
contradiction
then
O = O1
by A1, A42, A26, A34, A39, A29, INCPROJ:def 9;
hence
contradiction
by A6, A11, A18, A22, Def1;
verum
end;
A44:
p on O2
by A16, INCSP_1:12;
pp9 <> c
by A3, A19, A18, A28, A27, A24, A21, INCPROJ:def 9;
then A45:
A <> O2
by A7, A20, A35, A25, A23, INCPROJ:def 9;
A46:
q on O2
by A16, INCSP_1:12;
A47:
p <> d
by A5, A11, A18, A34, Def1;
q <> b
proof
assume
not
q <> b
;
contradiction
then
O2 = O3
by A4, A46, A25, A27, A24, A23, INCPROJ:def 9;
hence
contradiction
by A22, A39, A44, A28, A47, A37, INCPROJ:def 9;
verum
end;
hence
( q <> a & q <> b & not q on A & not q on Q )
by A26, A34, A39, A46, A44, A45, A37, A43, A41, INCPROJ:def 9; verum