reconsider B = IRRAT as Subset of R^1 by TOPMETR:17;
let A be Subset of R^1; :: thesis:
let a, b be Real; :: thesis:
assume A1: A = (].-infty,a.] \/ (IRRAT (a,b))) \/ [.b,+infty.[ ; :: thesis:
B c= A

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A2: x in B ; :: thesis:
then reconsider x9 = x as Real ;

suppose x9 <= a ; :: thesis:

then x9 in ].-infty,a.] by XXREAL_1:234;
then x9 in ].-infty,a.] \/ (IRRAT (a,b)) by XBOOLE_0:def 3;
hence x in A by A1, XBOOLE_0:def 3; :: thesis:

end;

suppose ( x9 > a & x9 < b ) ; :: thesis:

then x9 in ].a,b.[ by XXREAL_1:4;
then x9 in IRRAT /\ ].a,b.[ by A2, XBOOLE_0:def 4;
then x9 in IRRAT (a,b) by BORSUK_5:def 3;
then x9 in ].-infty,a.] \/ (IRRAT (a,b)) by XBOOLE_0:def 3;
hence x in A by A1, XBOOLE_0:def 3; :: thesis:

end;

suppose x9 >= b ; :: thesis:

then x9 in [.b,+infty.[ by XXREAL_1:236;
hence x in A by A1, XBOOLE_0:def 3; :: thesis:

end;

end;

end;

then A3: Cl B c= Cl A by PRE_TOPC:19;
Cl B = the carrier of R^1 by BORSUK_5:28;
hence Cl A = the carrier of R^1 by A3, XBOOLE_0:def 10; :: thesis: