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