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:
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:
ex F being Subset-Family of R^1 st
( F is closed & F is countable & A = union F )

take F ; :: thesis:
for B being Subset of R^1 st B in F holds
B is closed

end;

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

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

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

end;

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

end;

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in A ; :: thesis:
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:

end;

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in union F ; :: thesis:
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:

end;