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