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 )

( 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 )
;

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_{1}( Point of (TT | a)) -> Element of bool the carrier of (TT | a) = {$1};

defpred S_{1}[ set ] means verum;

defpred S_{2}[ set ] means ( $1 in A & S_{1}[$1] );

consider S being Subset-Family of (TT | a) such that

A3: S = { H_{1}(w) where w is Point of (TT | a) : S_{2}[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 )

[#] (TT | a) c= union S

A8: S is closed

card { H_{1}(w) where w is Point of (TT | a) : S_{2}[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;reconsider a = A as non empty Subset of TT by A2;

set Ta = TT | a;

deffunc H

defpred S

defpred S

consider S being Subset-Family of (TT | a) such that

A3: S = { H

for B being Subset of (TT | a) st B in S holds

( B is finite-ind & ind B <= 0 )

proof

then A5:
( S is finite-ind & ind S <= 0 )
by TOPDIM_1:11;
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_{1}(w)
and

S_{2}[w]
by A3;

card H_{1}(w) = 1
by CARD_1:30;

then ind H_{1}(w) < 1 + 0
by TOPDIM_1:8;

hence ( B is finite-ind & ind B <= 0 ) by A4, INT_1:7; :: thesis: verum

end;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

S

card H

then ind H

hence ( B is finite-ind & ind B <= 0 ) by A4, INT_1:7; :: thesis: verum

[#] (TT | a) c= union S

proof

then A7:
S is Cover of (TT | a)
by SETFAM_1:def 11;
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;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

A8: S is closed

proof

A9:
card A c= omega
by CARD_3:def 14;
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_{1}(w) & S_{2}[w] )
by A3;

hence B is closed by A1; :: thesis: verum

end;assume B in S ; :: thesis: B is closed

then ex w being Point of (TT | a) st

( B = H

hence B is closed by A1; :: thesis: verum

card { H

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