let A be Subset of R^1; :: thesis: for a, b being Real st a < b & A = IRRAT (a,b) holds
( a in Cl A & b in Cl A )
let a, b be Real; :: 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 13, XREAL_0:def 1;
for r being Real st r > 0 holds
Ball (a9,r) meets A
proof
set p = a;
let r be Real; :: thesis: ( r > 0 implies Ball (a9,r) meets A )
reconsider pp = a + r as Element of RealSpace by METRIC_1:def 13, 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:29; :: 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:226; :: thesis: verum
end;
end;
end;
then consider Q being irrational Real such that
A5: a < Q and
A6: Q < min (pp,((a + b) / 2)) by Th26;
(a + b) / 2 < b by A1, XREAL_1:226;
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:9;
reconsider P = Q as Element of RealSpace by METRIC_1:def 13, XREAL_0:def 1;
P - a < (min (pp,((a + b) / 2))) - a by A6, XREAL_1:9;
then P - a < r by A8, XXREAL_0:2;
then dist (a9,P) < r by A5, Th13;
then A9: P in Ball (a9,r) by METRIC_1:11;
Q in IRRAT by Th16;
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:92, TOPMETR:def 6; :: thesis: verum
end;
b in Cl A
proof
reconsider a9 = b as Element of RealSpace by METRIC_1:def 13, XREAL_0:def 1;
for r being Real st r > 0 holds
Ball (a9,r) meets A
proof
set p = b;
let r be Real; :: thesis: ( r > 0 implies Ball (a9,r) meets A )
reconsider pp = b - r as Element of RealSpace by METRIC_1:def 13, 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:29;
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:19; :: 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:226; :: thesis: verum
end;
end;
end;
then consider Q being irrational Real such that
A12: max (pp,((b + a) / 2)) < Q and
A13: Q < b by Th26;
(b + a) / 2 > a by A1, XREAL_1:226;
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:13;
reconsider P = Q as Element of RealSpace by METRIC_1:def 13, XREAL_0:def 1;
b - P < b - (max (pp,((b + a) / 2))) by A12, XREAL_1:10;
then b - P < r by A15, XXREAL_0:2;
then dist (a9,P) < r by A13, Th13;
then A16: P in Ball (a9,r) by METRIC_1:11;
Q in IRRAT by Th16;
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:92, TOPMETR:def 6; :: thesis: verum
end;
hence b in Cl A ; :: thesis: verum