reconsider B = IRRAT as Subset of R^1 by TOPMETR:17;
let A be Subset of R^1; 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; ( 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.[
; Cl A = the carrier of R^1
B c= A
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; verum