reconsider E = {{}} as Subset-Family of (T | A) by SETFAM_1:46;
defpred S₁[ object , object ] means ex D2 being set st
( D2 = A & D2 /\ A = T );
set TOP = the topology of T;
let FA be Subset-Family of (T | A); :: according to METRIZTS:def 2 :: thesis: ( FA is open & FA is Cover of (T | A) implies ex G being Subset-Family of (T | A) st
( G c= FA & G is Cover of (T | A) & G is countable ) )
assume that
A1: FA is open and
A2: FA is Cover of (T | A) ; :: thesis: ex G being Subset-Family of (T | A) st
( G c= FA & G is Cover of (T | A) & G is countable )
A3: for x being object st x in FA holds
ex y being object st
( y in the topology of T & S₁[x,y] )

proof

let x be object ; :: thesis: ( x in FA implies ex y being object st
( y in the topology of T & S₁[x,y] ) )
assume A4: x in FA ; :: thesis: ex y being object st
( y in the topology of T & S₁[x,y] )
reconsider X = x as Subset of (T | A) by A4;
X is open by A1, A4;
then X in the topology of (T | A) ;
then consider Q being Subset of T such that
A5: ( Q in the topology of T & X = Q /\ ([#] (T | A)) ) by PRE_TOPC:def 4;
take Q ; :: thesis: ( Q in the topology of T & S₁[x,Q] )
thus Q in the topology of T by A5; :: thesis: S₁[x,Q]
take Q ; :: thesis: ( Q = Q & Q /\ A = x )
thus ( Q = Q & Q /\ A = x ) by A5, PRE_TOPC:def 5; :: thesis: verum

end;

consider f being Function of FA, the topology of T such that
A6: for x being object st x in FA holds
S₁[x,f . x] from FUNCT_2:sch 1(A3);
A ` in the topology of T by PRE_TOPC:def 2;
then ( the topology of T is open & {(A `)} c= the topology of T ) by ZFMISC_1:31;
then reconsider RNG = rng f, AA = {(A `)} as open Subset-Family of T by TOPS_2:11, XBOOLE_1:1;
reconsider RA = RNG \/ AA as open Subset-Family of T by TOPS_2:13;
A7: A = [#] (T | A) by PRE_TOPC:def 5;
A8: dom f = FA by FUNCT_2:def 1;
[#] T c= union RA

proof

A9: A \/ (A `) = [#] the carrier of T by SUBSET_1:10;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in [#] T or x in union RA )
assume A10: x in [#] T ; :: thesis: x in union RA

per cases ( x in A or x in A ` ) by A9, A10, XBOOLE_0:def 3;

suppose A11: x in A ; :: thesis: x in union RA

A = union FA by A2, A7, SETFAM_1:45;
then consider y being set such that
A12: x in y and
A13: y in FA by A11, TARSKI:def 4;
f . y in RNG by A8, A13, FUNCT_1:def 3;
then A14: f . y in RA by XBOOLE_0:def 3;
S₁[y,f . y] by A6, A13;
then (f . y) /\ A = y ;
then x in f . y by A12, XBOOLE_0:def 4;
hence x in union RA by A14, TARSKI:def 4; :: thesis: verum

end;

suppose A15: x in A ` ; :: thesis: x in union RA

A ` in AA by TARSKI:def 1;
then A ` in RA by XBOOLE_0:def 3;
hence x in union RA by A15, TARSKI:def 4; :: thesis: verum

end;

end;

end;

then RA is Cover of T by SETFAM_1:def 11;
then consider G being Subset-Family of T such that
A16: G c= RA and
A17: G is Cover of T and
A18: G is countable by Def2;
set GA = G | A;
take GE = (G | A) \ E; :: thesis: ( GE c= FA & GE is Cover of (T | A) & GE is countable )
thus GE c= FA :: thesis: ( GE is Cover of (T | A) & GE is countable )

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in GE or x in FA )
assume A19: x in GE ; :: thesis: x in FA
then A20: x <> {} by ZFMISC_1:56;
x in G | A by A19, ZFMISC_1:56;
then consider R being Subset of T such that
A21: R in G and
A22: R /\ A = x by TOPS_2:def 3;

per cases ( R in RNG or R in AA ) by A16, A21, XBOOLE_0:def 3;

suppose R in RNG ; :: thesis: x in FA

then consider y being object such that
A23: y in dom f and
A24: f . y = R by FUNCT_1:def 3;
S₁[y,f . y] by A6, A23;
then y = R /\ A by A24;
hence x in FA by A22, A23; :: thesis: verum

end;

suppose R in AA ; :: thesis: x in FA

then R = A ` by TARSKI:def 1;
then x = A \ A by A22, SUBSET_1:13;
hence x in FA by A20, XBOOLE_1:37; :: thesis: verum

end;

end;

end;

union G = [#] T by A17, SETFAM_1:45;
then [#] (T | A) = union (G | A) by A7, TOPS_2:33
.= union GE by PARTIT1:2 ;
hence GE is Cover of (T | A) by SETFAM_1:def 11; :: thesis: GE is countable
A25: card (G | A) c= card G by Th7;
card G c= omega by A18;
then card (G | A) c= omega by A25;
then G | A is countable ;
hence GE is countable by CARD_3:95; :: thesis: verum