set TOP = the topology of TM;
set cTM = the carrier of TM;
let Am be Subset of TM; :: thesis:
assume A1: Am is open ; :: thesis:

suppose A2: TM is empty ; :: thesis:

reconsider E = {} as empty Subset-Family of TM by TOPGEN_4:18;
Am = union E by A2, ZFMISC_1:2;
hence Am is F_sigma by TOPGEN_4:def 6; :: thesis:

end;

suppose A3: not TM is empty ; :: thesis:

suppose Am = [#] TM ; :: thesis:

hence Am is F_sigma by A3; :: thesis:

end;

suppose A4: Am <> [#] TM ; :: thesis:

consider metr being Function of [: the carrier of TM, the carrier of TM:],REAL such that
A5: metr is_metric_of the carrier of TM and
A6: Family_open_set (SpaceMetr ( the carrier of TM,metr)) = the topology of TM by PCOMPS_1:def 8;
reconsider Tm = SpaceMetr ( the carrier of TM,metr) as non empty MetrSpace by A3, A5, PCOMPS_1:36;
set TTm = TopSpaceMetr Tm;
Am in the topology of (TopSpaceMetr Tm) by A1, A6;
then reconsider a = Am as open Subset of (TopSpaceMetr Tm) by PRE_TOPC:def 2;
({} (TopSpaceMetr Tm)) ` = [#] (TopSpaceMetr Tm) ;
then reconsider A9 = a ` as non empty closed Subset of (TopSpaceMetr Tm) by A3, A4, A5, PCOMPS_2:4;
defpred S₁[ object , object ] means for n being Nat st n = TM holds
c₂ = { p where p is Point of (TopSpaceMetr Tm) : (dist_min A9) . p < 1 / (2 |^ n) } ;
A7: for x being object st x in NAT holds
ex y being object st
( y in the topology of TM & S₁[x,y] )

let x be object ; :: thesis:
assume x in NAT ; :: thesis:
then reconsider n = x as Element of NAT ;
reconsider BallA = { p where p is Point of (TopSpaceMetr Tm) : (dist_min A9) . p < 1 / (2 |^ n) } as open Subset of (TopSpaceMetr Tm) by Lm4;
take BallA ; :: thesis:
thus ( BallA in the topology of TM & S₁[x,BallA] ) by A6, PRE_TOPC:def 2; :: thesis:

end;

consider p being sequence of the topology of TM such that
A8: for x being object st x in NAT holds
S₁[x,p . x] from FUNCT_2:sch 1(A7);
reconsider RNG = rng p as open Subset-Family of TM by TOPS_2:11, XBOOLE_1:1;
set Crng = COMPLEMENT RNG;
A9: dom p = NAT by FUNCT_2:def 1;
A10: [#] TM = [#] (TopSpaceMetr Tm) by A3, A5, PCOMPS_2:4;
A11: union (COMPLEMENT RNG) = Am

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis:

let x be object ; :: thesis:
assume A12: x in union (COMPLEMENT RNG) ; :: thesis:
then consider y being set such that
A13: x in y and
A14: y in COMPLEMENT RNG by TARSKI:def 4;
reconsider Y = y as Subset of TM by A14;
Y ` in RNG by A14, SETFAM_1:def 7;
then consider n being object such that
A15: n in dom p and
A16: p . n = Y ` by FUNCT_1:def 3;
reconsider n = n as Element of NAT by A15;
assume not x in Am ; :: thesis:
then x in A9 by A10, A12, XBOOLE_0:def 5;
then A17: ( 2 |^ n > 0 & (dist_min A9) . x = 0 ) by HAUSDORF:5, PREPOWER:6;
Y ` = { q where q is Point of (TopSpaceMetr Tm) : (dist_min A9) . q < 1 / (2 |^ n) } by A8, A16;
then x in Y ` by A10, A12, A17;
hence contradiction by A13, XBOOLE_0:def 5; :: thesis:

end;

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A18: x in Am ; :: thesis:
then reconsider q = x as Point of (TopSpaceMetr Tm) by A3, A5, PCOMPS_2:4;
( Cl A9 = A9 & not q in A9 ) by A18, PRE_TOPC:22, XBOOLE_0:def 5;
then A19: (dist_min A9) . q <> 0 by HAUSDORF:8;
(dist_min A9) . q >= 0 by JORDAN1K:9;
then consider n being Nat such that
A20: 1 / (2 |^ n) <= (dist_min A9) . q by A19, PREPOWER:92;
A21: n in NAT by ORDINAL1:def 12;
p . n in RNG by A9, FUNCT_1:def 3, A21;
then reconsider pn = p . n as Subset of TM ;
A22: pn = { s where s is Point of (TopSpaceMetr Tm) : (dist_min A9) . s < 1 / (2 |^ n) } by A8, A21;
for s being Point of (TopSpaceMetr Tm) st s = q holds
not 1 / (2 |^ n) > (dist_min A9) . s by A20;
then not q in pn by A22;
then A23: q in pn ` by A18, XBOOLE_0:def 5;
(pn `) ` in RNG by A9, FUNCT_1:def 3, A21;
then pn ` in COMPLEMENT RNG by SETFAM_1:def 7;
hence x in union (COMPLEMENT RNG) by A23, TARSKI:def 4; :: thesis:

end;

( COMPLEMENT RNG is closed & RNG is countable ) by A9, CARD_3:93, TOPS_2:10;
hence Am is F_sigma by A11, TOPGEN_4:def 6; :: thesis:

end;

end;

end;

end;