let T be TopSpace; :: thesis: 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; :: thesis: ( T | A is T_4 implies ( A is finite-ind & ind A <= 0 ) )
assume A1: T | A is T_4 ; :: thesis: ( A is finite-ind & ind A <= 0 )

per cases ( A = {} T or not A is empty ) ;

suppose A = {} T ; :: thesis: ( A is finite-ind & ind A <= 0 )

hence ( A is finite-ind & ind A <= 0 ) by TOPDIM_1:6; :: thesis: verum

end;

suppose A2: not A is empty ; :: thesis: ( 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 H₁( Point of (TT | a)) -> Element of bool the carrier of (TT | a) = {$1};
defpred S₁[ set ] means verum;
defpred S₂[ set ] means ( $1 in A & S₁[$1] );
consider S being Subset-Family of (TT | a) such that
A3: S = { H₁(w) where w is Point of (TT | a) : S₂[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 )

proof

let B be Subset of (TT | a); :: thesis: ( B in S implies ( B is finite-ind & ind B <= 0 ) )
assume B in S ; :: thesis: ( B is finite-ind & ind B <= 0 )
then consider w being Point of (TT | a) such that
A4: B = H₁(w) and
S₂[w] by A3;
card H₁(w) = 1 by CARD_1:30;
then ind H₁(w) < 1 + 0 by TOPDIM_1:8;
hence ( B is finite-ind & ind B <= 0 ) by A4, INT_1:7; :: thesis: verum

end;

then A5: ( S is finite-ind & ind S <= 0 ) by TOPDIM_1:11;
[#] (TT | a) c= union S

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in [#] (TT | a) or x in union S )
assume A6: x in [#] (TT | a) ; :: thesis: x in union S
then x in a by PRE_TOPC:def 5;
then ( x in {x} & {x} in S ) by A3, A6, TARSKI:def 1;
hence x in union S by TARSKI:def 4; :: thesis: verum

end;

then A7: S is Cover of (TT | a) by SETFAM_1:def 11;
A8: S is closed

proof

let B be Subset of (TT | a); :: according to TOPS_2:def 2 :: thesis: ( not B in S or B is closed )
assume B in S ; :: thesis: B is closed
then ex w being Point of (TT | a) st
( B = H₁(w) & S₂[w] ) by A3;
hence B is closed by A1; :: thesis: verum

end;

A9: card A c= omega by CARD_3:def 14;
card { H₁(w) where w is Point of (TT | a) : S₂[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; :: thesis: verum

end;

end;