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

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

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

then A3:
Cl B c= Cl A
by PRE_TOPC:19;
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 ;

end;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 )
;

end;

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;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

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;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

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