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