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
reconsider B = IRRAT as Subset of R^1 by TOPMETR:24;
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 x' = x as real number ;

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

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

then x' in ].-infty ,a.] by XXREAL_1:234;
then x' 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 ( x' > a & x' < b ) ; :: thesis: x in A

then x' in ].a,b.[ by XXREAL_1:4;
then x' in IRRAT /\ ].a,b.[ by A2, XBOOLE_0:def 4;
then x' in IRRAT a,b by BORSUK_5:def 5;
then x' 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 x' >= b ; :: thesis: x in A

then x' 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