let T be TopSpace; for A being countable Subset of T st T | A is T_4 holds
( A is finite-ind & ind A <= 0 )
let A be countable Subset of T; ( T | A is T_4 implies ( A is finite-ind & ind A <= 0 ) )
assume A1:
T | A is T_4
; ( A is finite-ind & ind A <= 0 )
per cases
( A = {} T or not A is empty )
;
suppose A2:
not
A is
empty
;
( A is finite-ind & ind A <= 0 )then reconsider TT =
T as non
empty TopSpace ;
reconsider a =
A as non
empty Subset of
TT by A2;
set Ta =
TT | a;
deffunc H1(
Point of
(TT | a))
-> Element of
bool the
carrier of
(TT | a) =
{$1};
defpred S1[
set ]
means verum;
defpred S2[
set ]
means ( $1
in A &
S1[$1] );
consider S being
Subset-Family of
(TT | a) such that A3:
S = { H1(w) where w is Point of (TT | a) : S2[w] }
from LMOD_7:sch 5();
for
B being
Subset of
(TT | a) st
B in S holds
(
B is
finite-ind &
ind B <= 0 )
then A5:
(
S is
finite-ind &
ind S <= 0 )
by TOPDIM_1:11;
[#] (TT | a) c= union S
then A7:
S is
Cover of
(TT | a)
by SETFAM_1:def 11;
A8:
S is
closed
A9:
card A c= omega
by CARD_3:def 14;
card { H1(w) where w is Point of (TT | a) : S2[w] } c= card A
from BORSUK_2:sch 1();
then
card S c= omega
by A3, A9;
then A10:
S is
countable
;
[#] (TT | a) = A
by PRE_TOPC:def 5;
then A11:
TT | a is
countable
by ORDERS_4:def 2;
then
TT | a is
finite-ind
by A1, A5, A7, A8, A10, TOPDIM_1:36;
then A12:
A is
finite-ind
by TOPDIM_1:18;
ind (TT | a) <= 0
by A1, A5, A7, A8, A10, A11, TOPDIM_1:36;
hence
(
A is
finite-ind &
ind A <= 0 )
by A12, TOPDIM_1:17;
verum end; end;