defpred S1[ object ] means ex a being Element of RAT st a = \$1;
defpred S2[ 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 & S2[x] ) ) from then consider F being set such that
A1: for x being set holds
( x in F iff ( x in bool RAT & S2[x] ) ) ;
A2: bool RAT c= bool REAL by ;
F c= bool the carrier of R^1 by ;
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 : S1[x] }
proof
thus F c= { {x} where x is Element of RAT : S1[x] } :: according to XBOOLE_0:def 10 :: thesis: { {x} where x is Element of RAT : S1[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 : S1[x] } )
assume y in F ; :: thesis: y in { {x} where x is Element of RAT : S1[x] }
then S2[y] by A1;
hence y in { {x} where x is Element of RAT : S1[x] } ; :: thesis: verum
end;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { {x} where x is Element of RAT : S1[x] } or y in F )
assume y in { {x} where x is Element of RAT : S1[x] } ; :: thesis: y in F
then ex z being Element of RAT st
( y = {z} & S1[z] ) ;
hence y in F by A1; :: thesis: verum
end;
{ {x} where x is Element of RAT : S1[x] } is countable from 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 ;
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