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 a9 = a as Element of RealSpace by METRIC_1:def 14, XREAL_0:def 1;
for r being real number st r > 0 holds
Ball a9,r meets A

proof

set p = a;
let r be real number ; :: thesis: ( r > 0 implies Ball a9,r meets 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);
A3: min pp,((a + b) / 2) <= (a + b) / 2 by XXREAL_0:17;
assume A4: r > 0 ; :: thesis: Ball a9,r meets A
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 A4, 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
A5: a < Q and
A6: Q < min pp,((a + b) / 2) by Th50;
(a + b) / 2 < b by A1, XREAL_1:228;
then min pp,((a + b) / 2) < b by A3, XXREAL_0:2;
then Q < b by A6, XXREAL_0:2;
then A7: Q in ].a,b.[ by A5, XXREAL_1:4;
min pp,((a + b) / 2) <= pp by XXREAL_0:17;
then A8: (min pp,((a + b) / 2)) - a <= pp - a by XREAL_1:11;
reconsider P = Q as Element of RealSpace by METRIC_1:def 14, XREAL_0:def 1;
P - a < (min pp,((a + b) / 2)) - a by A6, XREAL_1:11;
then P - a < r by A8, XXREAL_0:2;
then dist a9,P < r by A5, Th34;
then A9: P in Ball a9,r by METRIC_1:12;
Q in IRRAT by Th37;
then Q in A by A2, A7, XBOOLE_0:def 4;
hence Ball a9,r meets A by A9, 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 a9 = b as Element of RealSpace by METRIC_1:def 14, XREAL_0:def 1;
for r being real number st r > 0 holds
Ball a9,r meets A

proof

set p = b;
let r be real number ; :: thesis: ( r > 0 implies Ball a9,r meets A )
reconsider pp = b - r as Element of RealSpace by METRIC_1:def 14, XREAL_0:def 1;
set pr = max pp,((b + a) / 2);
A10: max pp,((b + a) / 2) >= (b + a) / 2 by XXREAL_0:25;
assume r > 0 ; :: thesis: Ball a9,r meets A
then A11: b < b + r by XREAL_1:31;
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
A12: max pp,((b + a) / 2) < Q and
A13: Q < b by Th50;
(b + a) / 2 > a by A1, XREAL_1:228;
then a < max pp,((b + a) / 2) by A10, XXREAL_0:2;
then a < Q by A12, XXREAL_0:2;
then A14: Q in ].a,b.[ by A13, XXREAL_1:4;
max pp,((b + a) / 2) >= pp by XXREAL_0:25;
then A15: b - (max pp,((b + a) / 2)) <= b - pp by XREAL_1:15;
reconsider P = Q as Element of RealSpace by METRIC_1:def 14, XREAL_0:def 1;
b - P < b - (max pp,((b + a) / 2)) by A12, XREAL_1:12;
then b - P < r by A15, XXREAL_0:2;
then dist a9,P < r by A13, Th34;
then A16: P in Ball a9,r by METRIC_1:12;
Q in IRRAT by Th37;
then Q in A by A2, A14, XBOOLE_0:def 4;
hence Ball a9,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