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 set ; :: 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 14, TOPMETR:24;

now

let r be real number ; :: thesis: ( r > 0 implies Ball p,r meets A )
reconsider pr = p + r as Element of RealSpace by METRIC_1:def 14, XREAL_0:def 1;
assume r > 0 ; :: thesis: Ball p,r meets A
then consider Q being real irrational number such that
A2: p < Q and
A3: Q < pr by Th50, XREAL_1:31;
reconsider P = Q as Element of RealSpace by METRIC_1:def 14, XREAL_0:def 1;
P - p < pr - p by A3, XREAL_1:11;
then dist p,P < r by A2, Th34;
then A4: P in Ball p,r by METRIC_1:12;
Q in A by A1, Th37;
hence Ball p,r meets A by A4, XBOOLE_0:3; :: thesis: verum

end;

hence x in Cl A by GOBOARD6:95, TOPMETR:def 7; :: thesis: verum

end;

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