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