defpred S₁[ object ] means ex a being Element of RAT st a = $1;
defpred S₂[ object ] means ex a being Element of RAT st {a} = $1;
let A be Subset of R^1; :: thesis: ( A = RAT implies A is F_sigma )
ex F being set st
for x being set holds
( x in F iff ( x in bool RAT & S₂[x] ) ) from XFAMILY:sch 1();
then consider F being set such that
A1: for x being set holds
( x in F iff ( x in bool RAT & S₂[x] ) ) ;
A2: bool RAT c= bool REAL by NUMBERS:12, ZFMISC_1:67;
F c= bool the carrier of R^1 by A1, A2, TOPMETR:17;
then reconsider F = F as Subset-Family of R^1 ;
assume A3: A = RAT ; :: thesis: A is F_sigma
ex F being Subset-Family of R^1 st
( F is closed & F is countable & A = union F )

proof

take F ; :: thesis: ( F is closed & F is countable & A = union F )
for B being Subset of R^1 st B in F holds
B is closed

proof

let B be Subset of R^1; :: thesis: ( B in F implies B is closed )
assume B in F ; :: thesis: B is closed
then ex a being Element of RAT st {a} = B by A1;
hence B is closed ; :: thesis: verum

end;

hence F is closed by TOPS_2:def 2; :: thesis: ( F is countable & A = union F )
A4: F = { {x} where x is Element of RAT : S₁[x] }

proof

thus F c= { {x} where x is Element of RAT : S₁[x] } :: according to XBOOLE_0:def 10 :: thesis: { {x} where x is Element of RAT : S₁[x] } c= F

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in F or y in { {x} where x is Element of RAT : S₁[x] } )
assume y in F ; :: thesis: y in { {x} where x is Element of RAT : S₁[x] }
then S₂[y] by A1;
hence y in { {x} where x is Element of RAT : S₁[x] } ; :: thesis: verum

end;

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { {x} where x is Element of RAT : S₁[x] } or y in F )
assume y in { {x} where x is Element of RAT : S₁[x] } ; :: thesis: y in F
then ex z being Element of RAT st
( y = {z} & S₁[z] ) ;
hence y in F by A1; :: thesis: verum

end;

{ {x} where x is Element of RAT : S₁[x] } is countable from TOPGEN_4:sch 1();
hence F is countable by A4; :: thesis: A = union F
thus A c= union F :: according to XBOOLE_0:def 10 :: thesis: union F c= A

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in union F )
assume x in A ; :: thesis: x in union F
then reconsider x = x as Element of RAT by A3;
( {x} in F & x in {x} ) by A1, TARSKI:def 1;
hence x in union F by TARSKI:def 4; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union F or x in A )
assume x in union F ; :: thesis: x in A
then consider Y being set such that
A5: x in Y and
A6: Y in F by TARSKI:def 4;
ex a being Element of RAT st {a} = Y by A1, A6;
hence x in A by A3, A5; :: thesis: verum

end;

hence A is F_sigma ; :: thesis: verum