let IPP be Fanoian IncProjSp; :: thesis: 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_different & d on A & c,d,p,q are_mutually_different )
consider r being POINT of IPP, A being LINE of IPP such that
A1:
not r on A
by INCPROJ:def 11;
consider p, q, c being POINT of IPP such that
A2:
( p <> q & q <> c & c <> p & p on A & q on A & c on A )
by INCPROJ:def 12;
consider B being LINE of IPP such that
A3:
( r on B & c on B )
by INCPROJ:def 10;
consider s being POINT of IPP such that
A4:
( s on B & s <> r & s <> c )
by Th8;
consider Q being LINE of IPP such that
A5:
( r on Q & q on Q )
by INCPROJ:def 10;
consider L being LINE of IPP such that
A6:
( p on L & s on L )
by INCPROJ:def 10;
consider S being LINE of IPP such that
A7:
( p on S & r on S )
by INCPROJ:def 10;
consider R being LINE of IPP such that
A8:
( q on R & s on R )
by INCPROJ:def 10;
A9:
R <> Q
then A10:
not r on R
by A1, A2, A5, A8, INCPROJ:def 9;
A11:
not p on Q
by A1, A2, A5, INCPROJ:def 9;
A12:
not q on S
by A1, A2, A7, INCPROJ:def 9;
A13:
not q on L
A14:
not p on R
A15:
not c on Q
by A1, A2, A5, INCPROJ:def 9;
not c on L
then consider a being POINT of IPP such that
A16:
( a on Q & a on L )
by A1, A2, A3, A4, A5, A6, A15, INCPROJ:def 13;
A17:
not c on R
by A2, A8, A14, INCPROJ:def 9;
A18:
not c on S
by A1, A2, A7, INCPROJ:def 9;
then consider b being POINT of IPP such that
A19:
( b on R & b on S )
by A1, A2, A3, A4, A7, A8, A17, INCPROJ:def 13;
consider C being LINE of IPP such that
A20:
( a on C & b on C )
by INCPROJ:def 10;
A21:
not s on Q
by A3, A4, A5, A15, INCPROJ:def 9;
A22:
S <> L
by A3, A4, A6, A7, A18, INCPROJ:def 9;
then A23:
not r on L
by A1, A2, A6, A7, INCPROJ:def 9;
A24:
not s on S
by A3, A4, A7, A18, INCPROJ:def 9;
A25:
( {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 )
by A2, A3, A4, A5, A6, A7, A8, A16, A19, INCSP_1:12;
A26:
{a,b} on C
by A20, INCSP_1:11;
then A27:
not c on C
by A10, A11, A12, A13, A14, A21, A23, A24, A25, INCPROJ:def 18;
consider D being LINE of IPP such that
A28:
( b on D & c on D )
by INCPROJ:def 10;
A29:
a <> s
by A3, A4, A5, A15, A16, INCPROJ:def 9;
A30:
a <> r
by A1, A2, A6, A7, A16, A22, INCPROJ:def 9;
A31:
S <> Q
by A1, A2, A5, A7, INCPROJ:def 9;
A32:
not a on S
by A5, A7, A12, A16, A30, INCPROJ:def 9;
A33:
S <> D
by A1, A2, A7, A28, INCPROJ:def 9;
A34:
R <> D
by A2, A8, A14, A28, INCPROJ:def 9;
A35:
R <> C
by A6, A8, A14, A16, A20, A29, INCPROJ:def 9;
A36:
S <> C
by A5, A7, A12, A16, A20, A30, INCPROJ:def 9;
A37:
C,D,R,S are_mutually_different
by A7, A14, A20, A27, A28, A32, A33, A34, A35, ZFMISC_1:def 6;
A38:
not b on Q
by A5, A8, A9, A12, A19, INCPROJ:def 9;
then
not r on C
by A5, A16, A20, A30, INCPROJ:def 9;
then consider d being POINT of IPP such that
A39:
( d on A & d on C )
by A1, A2, A5, A7, A16, A19, A20, A31, INCPROJ:def 13;
A40:
d <> q
by A5, A13, A16, A20, A38, A39, INCPROJ:def 9;
d <> p
by A7, A14, A19, A20, A36, A39, INCPROJ:def 9;
then
c,d,p,q are_mutually_different
by A2, A27, A39, A40, 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_different & d on A & c,d,p,q are_mutually_different )
by A10, A11, A12, A13, A14, A21, A23, A24, A25, A26, A27, A28, A37, A39; :: thesis: verum