defpred S_{1}[ object ] means ex a being Element of RAT st a = $1;

defpred S_{2}[ 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_{2}[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_{2}[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 )

defpred S

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

then consider F being set such that

A1: for x being set holds

( x in F iff ( x in bool RAT & S

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

hence
A is F_sigma
; :: thesis: verum
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

A4: F = { {x} where x is Element of RAT : S_{1}[x] }
_{1}[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

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;for B being Subset of R^1 st B in F holds

B is closed

proof

hence
F is closed
by TOPS_2:def 2; :: thesis: ( F is countable & A = union F )
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;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

A4: F = { {x} where x is Element of RAT : S

proof

{ {x} where x is Element of RAT : S
thus
F c= { {x} where x is Element of RAT : S_{1}[x] }
:: according to XBOOLE_0:def 10 :: thesis: { {x} where x is Element of RAT : S_{1}[x] } c= F_{1}[x] } or y in F )

assume y in { {x} where x is Element of RAT : S_{1}[x] }
; :: thesis: y in F

then ex z being Element of RAT st

( y = {z} & S_{1}[z] )
;

hence y in F by A1; :: thesis: verum

end;proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { {x} where x is Element of RAT : S
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_{1}[x] } )

assume y in F ; :: thesis: y in { {x} where x is Element of RAT : S_{1}[x] }

then S_{2}[y]
by A1;

hence y in { {x} where x is Element of RAT : S_{1}[x] }
; :: thesis: verum

end;assume y in F ; :: thesis: y in { {x} where x is Element of RAT : S

then S

hence y in { {x} where x is Element of RAT : S

assume y in { {x} where x is Element of RAT : S

then ex z being Element of RAT st

( y = {z} & S

hence y in F by A1; :: thesis: verum

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 union F or x in A )
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;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

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