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

proof

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

per cases ( x9 <= a or ( x9 > a & x9 < b ) or x9 >= b ) ;

suppose x9 <= a ; :: thesis: x in A

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: verum

end;

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

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: verum

end;

suppose x9 >= b ; :: thesis: x in A

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

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: verum