let A be Subset of R^1 ; :: thesis: for a, b being real number st a < b & A = IRRAT a,b holds
( a in Cl A & b in Cl A )
let a, b be real number ; :: thesis: ( a < b & A = IRRAT a,b implies ( a in Cl A & b in Cl A ) )
assume that
A1: a < b and
A2: A = IRRAT a,b ; :: thesis: ( a in Cl A & b in Cl A )
thus a in Cl A :: thesis: b in Cl A

proof

reconsider a' = a as Element of RealSpace by METRIC_1:def 14, XREAL_0:def 1;
for r being real number st r > 0 holds
Ball a',r meets A

proof

let r be real number ; :: thesis: ( r > 0 implies Ball a',r meets A )
assume A3: r > 0 ; :: thesis: Ball a',r meets A
set p = a;
reconsider pp = a + r as Element of RealSpace by METRIC_1:def 14, XREAL_0:def 1;
set pr = min pp,((a + b) / 2);
A4: min pp,((a + b) / 2) <= (a + b) / 2 by XXREAL_0:17;
A5: (a + b) / 2 < b by A1, XREAL_1:228;
a < min pp,((a + b) / 2)

proof

per cases ( min pp,((a + b) / 2) = pp or min pp,((a + b) / 2) = (a + b) / 2 ) by XXREAL_0:15;

suppose min pp,((a + b) / 2) = pp ; :: thesis: a < min pp,((a + b) / 2)

hence a < min pp,((a + b) / 2) by A3, XREAL_1:31; :: thesis: verum

end;

suppose min pp,((a + b) / 2) = (a + b) / 2 ; :: thesis: a < min pp,((a + b) / 2)

hence a < min pp,((a + b) / 2) by A1, XREAL_1:228; :: thesis: verum

end;

end;

end;

then consider Q being real irrational number such that
A6: ( a < Q & Q < min pp,((a + b) / 2) ) by Th50;
A7: Q in IRRAT by Th37;
min pp,((a + b) / 2) < b by A4, A5, XXREAL_0:2;
then ( a < Q & Q < b ) by A6, XXREAL_0:2;
then Q in ].a,b.[ by XXREAL_1:4;
then A8: Q in A by A2, A7, XBOOLE_0:def 4;
reconsider P = Q as Element of RealSpace by METRIC_1:def 14, XREAL_0:def 1;
A9: P - a < (min pp,((a + b) / 2)) - a by A6, XREAL_1:11;
(min pp,((a + b) / 2)) - a <= r

proof

min pp,((a + b) / 2) <= pp by XXREAL_0:17;
then (min pp,((a + b) / 2)) - a <= pp - a by XREAL_1:11;
hence (min pp,((a + b) / 2)) - a <= r ; :: thesis: verum

end;

then P - a < r by A9, XXREAL_0:2;
then dist a',P < r by A6, Th34;
then P in Ball a',r by METRIC_1:12;
hence Ball a',r meets A by A8, XBOOLE_0:3; :: thesis: verum

end;

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

end;

b in Cl A

proof

reconsider a' = b as Element of RealSpace by METRIC_1:def 14, XREAL_0:def 1;
for r being real number st r > 0 holds
Ball a',r meets A

proof

let r be real number ; :: thesis: ( r > 0 implies Ball a',r meets A )
assume A10: r > 0 ; :: thesis: Ball a',r meets A
set p = b;
reconsider pp = b - r as Element of RealSpace by METRIC_1:def 14, XREAL_0:def 1;
set pr = max pp,((b + a) / 2);
A11: b < b + r by A10, XREAL_1:31;
A12: max pp,((b + a) / 2) >= (b + a) / 2 by XXREAL_0:25;
A13: (b + a) / 2 > a by A1, XREAL_1:228;
b > max pp,((b + a) / 2)

proof

per cases ( max pp,((b + a) / 2) = pp or max pp,((b + a) / 2) = (b + a) / 2 ) by XXREAL_0:16;

suppose max pp,((b + a) / 2) = pp ; :: thesis: b > max pp,((b + a) / 2)

hence b > max pp,((b + a) / 2) by A11, XREAL_1:21; :: thesis: verum

end;

suppose max pp,((b + a) / 2) = (b + a) / 2 ; :: thesis: b > max pp,((b + a) / 2)

hence b > max pp,((b + a) / 2) by A1, XREAL_1:228; :: thesis: verum

end;

end;

end;

then consider Q being real irrational number such that
A14: ( max pp,((b + a) / 2) < Q & Q < b ) by Th50;
A15: Q in IRRAT by Th37;
a < max pp,((b + a) / 2) by A12, A13, XXREAL_0:2;
then ( a < Q & Q < b ) by A14, XXREAL_0:2;
then Q in ].a,b.[ by XXREAL_1:4;
then A16: Q in A by A2, A15, XBOOLE_0:def 4;
reconsider P = Q as Element of RealSpace by METRIC_1:def 14, XREAL_0:def 1;
A17: b - P < b - (max pp,((b + a) / 2)) by A14, XREAL_1:12;
b - (max pp,((b + a) / 2)) <= r

proof

max pp,((b + a) / 2) >= pp by XXREAL_0:25;
then b - (max pp,((b + a) / 2)) <= b - pp by XREAL_1:15;
hence b - (max pp,((b + a) / 2)) <= r ; :: thesis: verum

end;

then b - P < r by A17, XXREAL_0:2;
then dist a',P < r by A14, Th34;
then P in Ball a',r by METRIC_1:12;
hence Ball a',r meets A by A16, XBOOLE_0:3; :: thesis: verum

end;

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

end;

hence b in Cl A ; :: thesis: verum