let IPP be Fanoian IncProjSp; ex p, q, r, s, a, b, c being POINT of IPP ex A, B, C, Q, L, R, S, D being LINE of IPP ex d being POINT of IPP st
( not q on L & not r on L & not p on Q & not s on Q & not p on R & not r on R & not q on S & not s on S & {a,p,s} on L & {a,q,r} on Q & {b,q,s} on R & {b,p,r} on S & {c,p,q} on A & {c,r,s} on B & {a,b} on C & not c on C & b on D & c on D & C,D,R,S are_mutually_distinct & d on A & c,d,p,q are_mutually_distinct )
consider r being POINT of IPP, A being LINE of IPP such that
A1:
not r on A
by INCPROJ:def 6;
consider p, q, c being POINT of IPP such that
A2:
p <> q
and
A3:
q <> c
and
A4:
c <> p
and
A5:
p on A
and
A6:
q on A
and
A7:
c on A
by INCPROJ:def 7;
consider B being LINE of IPP such that
A8:
r on B
and
A9:
c on B
by INCPROJ:def 5;
consider s being POINT of IPP such that
A10:
s on B
and
A11:
s <> r
and
A12:
s <> c
by Th8;
consider L being LINE of IPP such that
A13:
p on L
and
A14:
s on L
by INCPROJ:def 5;
consider Q being LINE of IPP such that
A15:
r on Q
and
A16:
q on Q
by INCPROJ:def 5;
A17:
not p on Q
by A1, A2, A5, A6, A15, A16, INCPROJ:def 4;
A18:
not c on Q
by A1, A3, A6, A7, A15, A16, INCPROJ:def 4;
then A19:
not s on Q
by A8, A9, A10, A11, A15, INCPROJ:def 4;
not c on L
proof
assume
c on L
;
contradiction
then
p on B
by A9, A10, A12, A13, A14, INCPROJ:def 4;
hence
contradiction
by A1, A4, A5, A7, A8, A9, INCPROJ:def 4;
verum
end;
then consider a being POINT of IPP such that
A20:
a on Q
and
A21:
a on L
by A1, A5, A6, A7, A8, A9, A10, A15, A16, A13, A14, A18, INCPROJ:def 8;
A22:
{a,p,s} on L
by A13, A14, A21, INCSP_1:2;
consider R being LINE of IPP such that
A23:
q on R
and
A24:
s on R
by INCPROJ:def 5;
consider S being LINE of IPP such that
A25:
p on S
and
A26:
r on S
by INCPROJ:def 5;
A27:
not c on S
by A1, A4, A5, A7, A25, A26, INCPROJ:def 4;
then A28:
not s on S
by A8, A9, A10, A11, A26, INCPROJ:def 4;
A29:
S <> L
by A8, A9, A10, A11, A14, A26, A27, INCPROJ:def 4;
then A30:
not r on L
by A1, A5, A13, A25, A26, INCPROJ:def 4;
A31:
S <> Q
by A1, A2, A5, A6, A15, A16, A25, INCPROJ:def 4;
A32:
not q on S
by A1, A2, A5, A6, A25, A26, INCPROJ:def 4;
A33:
not q on L
proof
assume
q on L
;
contradiction
then
s on A
by A2, A5, A6, A13, A14, INCPROJ:def 4;
hence
contradiction
by A1, A7, A8, A9, A10, A12, INCPROJ:def 4;
verum
end;
A34:
not p on R
proof
assume
p on R
;
contradiction
then
s on A
by A2, A5, A6, A23, A24, INCPROJ:def 4;
hence
contradiction
by A1, A7, A8, A9, A10, A12, INCPROJ:def 4;
verum
end;
then
not c on R
by A3, A5, A6, A7, A23, INCPROJ:def 4;
then consider b being POINT of IPP such that
A35:
b on R
and
A36:
b on S
by A1, A5, A6, A7, A8, A9, A10, A25, A26, A23, A24, A27, INCPROJ:def 8;
A37:
{b,q,s} on R
by A23, A24, A35, INCSP_1:2;
A38:
R <> Q
proof
assume
not
R <> Q
;
contradiction
then
B = Q
by A8, A10, A11, A15, A24, INCPROJ:def 4;
hence
contradiction
by A1, A3, A6, A7, A8, A9, A16, INCPROJ:def 4;
verum
end;
then A39:
not r on R
by A1, A6, A15, A16, A23, INCPROJ:def 4;
A40:
{c,r,s} on B
by A8, A9, A10, INCSP_1:2;
A41:
{b,p,r} on S
by A25, A26, A36, INCSP_1:2;
A42:
a <> r
by A1, A5, A13, A25, A26, A21, A29, INCPROJ:def 4;
then A43:
not a on S
by A15, A16, A26, A32, A20, INCPROJ:def 4;
A44:
{a,q,r} on Q
by A15, A16, A20, INCSP_1:2;
consider C being LINE of IPP such that
A45:
a on C
and
A46:
b on C
by INCPROJ:def 5;
a <> s
by A8, A9, A10, A11, A15, A18, A20, INCPROJ:def 4;
then A47:
R <> C
by A13, A14, A24, A34, A21, A45, INCPROJ:def 4;
A48:
not b on Q
by A16, A23, A38, A32, A35, A36, INCPROJ:def 4;
then
not r on C
by A15, A20, A45, A46, A42, INCPROJ:def 4;
then consider d being POINT of IPP such that
A49:
d on A
and
A50:
d on C
by A1, A5, A6, A15, A16, A25, A26, A20, A36, A45, A46, A31, INCPROJ:def 8;
S <> C
by A15, A16, A26, A32, A20, A45, A42, INCPROJ:def 4;
then A51:
d <> p
by A25, A34, A35, A36, A46, A50, INCPROJ:def 4;
A52:
{c,p,q} on A
by A5, A6, A7, INCSP_1:2;
A53:
{a,b} on C
by A45, A46, INCSP_1:1;
then A54:
not c on C
by A39, A17, A32, A33, A34, A19, A30, A28, A22, A44, A37, A41, A52, A40, INCPROJ:def 12;
consider D being LINE of IPP such that
A55:
b on D
and
A56:
c on D
by INCPROJ:def 5;
A57:
R <> D
by A3, A5, A6, A7, A23, A34, A56, INCPROJ:def 4;
d <> q
by A16, A33, A20, A21, A45, A46, A48, A50, INCPROJ:def 4;
then A58:
c,d,p,q are_mutually_distinct
by A2, A3, A4, A54, A50, A51, ZFMISC_1:def 6;
S <> D
by A1, A4, A5, A7, A25, A26, A56, INCPROJ:def 4;
then
C,D,R,S are_mutually_distinct
by A25, A34, A45, A54, A56, A43, A57, A47, ZFMISC_1:def 6;
hence
ex p, q, r, s, a, b, c being POINT of IPP ex A, B, C, Q, L, R, S, D being LINE of IPP ex d being POINT of IPP st
( not q on L & not r on L & not p on Q & not s on Q & not p on R & not r on R & not q on S & not s on S & {a,p,s} on L & {a,q,r} on Q & {b,q,s} on R & {b,p,r} on S & {c,p,q} on A & {c,r,s} on B & {a,b} on C & not c on C & b on D & c on D & C,D,R,S are_mutually_distinct & d on A & c,d,p,q are_mutually_distinct )
by A39, A17, A32, A33, A34, A19, A30, A28, A22, A44, A37, A41, A52, A40, A53, A54, A55, A56, A49, A58; verum