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 )
defpred S₁[ set , set ] means A /\ A = T;
A3: for x being set st x in FA holds
ex y being set st
( y in the topology of T & S₁[x,y] )

proof

let x be set ; :: thesis: ( x in FA implies ex y being set st
( y in the topology of T & S₁[x,y] ) )
assume A4: x in FA ; :: thesis: ex y being set 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, TOPS_2:def 1;
then X in the topology of (T | A) by PRE_TOPC:def 5;
then consider Q being Subset of T such that
A5: ( Q in the topology of T & X = Q /\ ([#] (T | A)) ) by PRE_TOPC:def 9;
take Q ; :: thesis: ( Q in the topology of T & S₁[x,Q] )
thus ( Q in the topology of T & S₁[x,Q] ) by A5, PRE_TOPC:def 10; :: thesis: verum

end;

consider f being Function of FA,the topology of T such that
A6: for x being set 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 5;
then ( the topology of T is open & {(A ` )} c= the topology of T ) by CANTOR_1:3, ZFMISC_1:37;
then reconsider RNG = rng f, AA = {(A ` )} as open Subset-Family of T by TOPS_2:18, XBOOLE_1:1;
reconsider RA = RNG \/ AA as open Subset-Family of T by TOPS_2:20;
A7: A = [#] (T | A) by PRE_TOPC:def 10;
A8: dom f = FA by FUNCT_2:def 1;
[#] T c= union RA

proof

A9: A \/ (A ` ) = [#] the carrier of T by SUBSET_1:25;
let x be set ; :: 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:60;
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 5;
then A14: f . y in RA by XBOOLE_0:def 3;
(f . y) /\ A = y by A6, A13;
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 12;
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;
reconsider E = {{} } as Subset-Family of (T | A) by SETFAM_1:61;
A19: card G c= omega by A18, CARD_3:def 15;
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 set ; :: according to TARSKI:def 3 :: thesis: ( not x in GE or x in FA )
assume A20: x in GE ; :: thesis: x in FA
then A21: x <> {} by ZFMISC_1:64;
x in G | A by A20, ZFMISC_1:64;
then consider R being Subset of T such that
A22: R in G and
A23: R /\ A = x by TOPS_2:def 3;

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

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

then consider y being set such that
A24: y in dom f and
A25: f . y = R by FUNCT_1:def 5;
y = R /\ A by A6, A24, A25;
hence x in FA by A23, A24; :: thesis: verum

end;

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

then R = A ` by TARSKI:def 1;
then x = A \ A by A23, SUBSET_1:32;
hence x in FA by A21, XBOOLE_1:37; :: thesis: verum

end;

end;

end;

union G = [#] T by A17, SETFAM_1:60;
then [#] (T | A) = union (G | A) by A7, TOPS_2:43
.= union GE by PARTIT1:3 ;
hence GE is Cover of (T | A) by SETFAM_1:def 12; :: thesis: GE is countable
card (G | A) c= card G by Th7;
then card (G | A) c= omega by A19, XBOOLE_1:1;
then G | A is countable by CARD_3:def 15;
hence GE is countable by CARD_3:130; :: thesis: verum