let A be Subset of R^1; :: thesis: ( A = IRRAT implies Cl A = the carrier of R^1 )
assume A1: A = IRRAT ; :: thesis: Cl A = the carrier of R^1
the carrier of R^1 c= Cl A

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of R^1 or x in Cl A )
assume x in the carrier of R^1 ; :: thesis: x in Cl A
then reconsider p = x as Element of RealSpace by METRIC_1:def 13, TOPMETR:17;

now :: thesis: for r being Real st r > 0 holds
Ball (p,r) meets A

let r be Real; :: thesis: ( r > 0 implies Ball (p,r) meets A )
reconsider pr = p + r as Element of RealSpace by METRIC_1:def 13, XREAL_0:def 1;
assume r > 0 ; :: thesis: Ball (p,r) meets A
then consider Q being irrational Real such that
A2: p < Q and
A3: Q < pr by Th26, XREAL_1:29;
reconsider P = Q as Element of RealSpace by METRIC_1:def 13, XREAL_0:def 1;
P - p < pr - p by A3, XREAL_1:9;
then dist (p,P) < r by A2, Th13;
then A4: P in Ball (p,r) by METRIC_1:11;
Q in A by A1, Th16;
hence Ball (p,r) meets A by A4, XBOOLE_0:3; :: thesis: verum

end;

hence x in Cl A by GOBOARD6:92, TOPMETR:def 6; :: thesis: verum

end;

hence Cl A = the carrier of R^1 by XBOOLE_0:def 10; :: thesis: verum