reconsider B = IRRAT as Subset of R^1 by TOPMETR:24;
let A be Subset of R^1 ; :: thesis: for a, b being real number st A = (].-infty ,a.] \/ (IRRAT a,b)) \/ [.b,+infty .[ holds
Cl A = the carrier of R^1
let a, b be real number ; :: 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 set ; :: 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 number ;

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 5;
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:49;
Cl B = the carrier of R^1 by BORSUK_5:51;
hence Cl A = the carrier of R^1 by A3, XBOOLE_0:def 10; :: thesis: verum