let Tf be finite-ind TopSpace; for A being Subset of Tf holds
( Tf | A is finite-ind & ind (Tf | A) <= ind Tf )
defpred S1[ Nat] means for T being TopSpace st T is finite-ind & ind T = $1 - 1 holds
for A being Subset of T holds
( T | A is finite-ind & ind (T | A) <= ind T );
[#] Tf is finite-ind
by Def4;
then reconsider i = (ind Tf) + 1 as Nat by Lm3;
A1:
for k being Nat st ( for n being Nat st n < k holds
S1[n] ) holds
S1[k]
proof
let n9 be
Nat;
( ( for n being Nat st n < n9 holds
S1[n] ) implies S1[n9] )
assume A2:
for
n being
Nat st
n < n9 holds
S1[
n]
;
S1[n9]
per cases
( n9 = 0 or n9 > 0 )
;
suppose
n9 > 0
;
S1[n9]then reconsider n =
n9 - 1 as
Nat by NAT_1:20;
let T be
TopSpace;
( T is finite-ind & ind T = n9 - 1 implies for A being Subset of T holds
( T | A is finite-ind & ind (T | A) <= ind T ) )assume that A6:
T is
finite-ind
and A7:
ind T = n9 - 1
;
for A being Subset of T holds
( T | A is finite-ind & ind (T | A) <= ind T )let A be
Subset of
T;
( T | A is finite-ind & ind (T | A) <= ind T )set TA =
T | A;
A8:
[#] (T | A) = A
by PRE_TOPC:def 5;
A9:
now for p being Point of (T | A)
for U being open Subset of (T | A) st p in U holds
ex W being open Subset of (T | A) st
( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= n - 1 )let p be
Point of
(T | A);
for U being open Subset of (T | A) st p in U holds
ex W being open Subset of (T | A) st
( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= n - 1 )let U be
open Subset of
(T | A);
( p in U implies ex W being open Subset of (T | A) st
( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= n - 1 ) )assume A10:
p in U
;
ex W being open Subset of (T | A) st
( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= n - 1 )
U in the
topology of
(T | A)
by PRE_TOPC:def 2;
then consider U9 being
Subset of
T such that A11:
U9 in the
topology of
T
and A12:
U = U9 /\ ([#] (T | A))
by PRE_TOPC:def 4;
A13:
p in U9
by A10, A12, XBOOLE_0:def 4;
then reconsider p9 =
p as
Point of
T ;
U9 is
open Subset of
T
by A11, PRE_TOPC:def 2;
then consider W9 being
open Subset of
T such that A14:
(
p9 in W9 &
W9 c= U9 )
and A15:
Fr W9 is
finite-ind
and A16:
ind (Fr W9) <= n - 1
by A6, A7, A13, Th16;
reconsider i =
(ind (Fr W9)) + 1 as
Nat by A15, Lm3;
((ind (Fr W9)) + 1) - 1
<= n - 1
by A16;
then
(
n9 - 1
< n9 - 0 &
(ind (Fr W9)) + 1
<= n9 - 1 )
by XREAL_1:9, XREAL_1:10;
then
(ind (Fr W9)) + 1
< n9
by XXREAL_0:2;
then A17:
S1[
i]
by A2;
reconsider W =
W9 /\ ([#] (T | A)) as
Subset of
(T | A) ;
W9 in the
topology of
T
by PRE_TOPC:def 2;
then
W in the
topology of
(T | A)
by PRE_TOPC:def 4;
then reconsider W =
W as
open Subset of
(T | A) by PRE_TOPC:def 2;
set FR9 =
Fr W9;
set TF =
T | (Fr W9);
(
[#] (T | (Fr W9)) = Fr W9 &
Fr W c= (Fr W9) /\ A )
by A8, Th1, PRE_TOPC:def 5;
then reconsider FrW =
Fr W as
Subset of
(T | (Fr W9)) by XBOOLE_1:18;
take W =
W;
( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= n - 1 )
[#] (T | (Fr W9)) c= [#] T
by PRE_TOPC:def 4;
then reconsider FrW9 =
FrW as
Subset of
T by XBOOLE_1:1;
A18:
(
T | (Fr W9) is
finite-ind &
ind (T | (Fr W9)) = ind (Fr W9) )
by A15, Lm5;
then
(T | (Fr W9)) | FrW is
finite-ind
by A17;
then A19:
[#] ((T | (Fr W9)) | FrW) is
finite-ind
;
ind ((T | (Fr W9)) | FrW) <= ind (Fr W9)
by A17, A18;
then
ind ([#] ((T | (Fr W9)) | FrW)) <= n - 1
by A16, XXREAL_0:2;
then
(
[#] ((T | (Fr W9)) | FrW) = FrW &
[#] ((T | (Fr W9)) | FrW) in (Seq_of_ind ((T | (Fr W9)) | FrW)) . n )
by A19, Th7, PRE_TOPC:def 5;
then
FrW in (Seq_of_ind (T | (Fr W9))) . n
by Th3;
then
FrW9 in (Seq_of_ind T) . n
by Th3;
then A20:
Fr W in (Seq_of_ind (T | A)) . n
by Th3;
then
Fr W is
finite-ind
;
hence
(
p in W &
W c= U &
Fr W is
finite-ind &
ind (Fr W) <= n - 1 )
by A10, A12, A14, A20, Th7, XBOOLE_0:def 4, XBOOLE_1:26;
verum end; then
T | A is
finite-ind
by Th15;
hence
(
T | A is
finite-ind &
ind (T | A) <= ind T )
by A7, A9, Th16;
verum end;
end;
for n being Nat holds S1[n]
from NAT_1:sch 4(A1);
then
S1[i]
;
hence
for A being Subset of Tf holds
( Tf | A is finite-ind & ind (Tf | A) <= ind Tf )
; verum