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