let A be Subset of R^1; for a, b being Real st a < b & A = IRRAT (a,b) holds
Cl A = [.a,b.]
let a, b be Real; ( a < b & A = IRRAT (a,b) implies Cl A = [.a,b.] )
assume that
A1:
a < b
and
A2:
A = IRRAT (a,b)
; Cl A = [.a,b.]
reconsider ab = ].a,b.[, RT = IRRAT as Subset of R^1 by TOPMETR:17;
reconsider RR = IRRAT /\ ].a,b.[ as Subset of R^1 by TOPMETR:17;
A3:
the carrier of R^1 /\ (Cl ab) = Cl ab
by XBOOLE_1:28;
A4:
Cl RR c= (Cl RT) /\ (Cl ab)
by PRE_TOPC:21;
thus
Cl A c= [.a,b.]
XBOOLE_0:def 10 [.a,b.] c= Cl A
thus
[.a,b.] c= Cl A
verumproof
let x be
object ;
TARSKI:def 3 ( not x in [.a,b.] or x in Cl A )
assume A5:
x in [.a,b.]
;
x in Cl A
then reconsider p =
x as
Element of
RealSpace by METRIC_1:def 13;
A6:
a <= p
by A5, XXREAL_1:1;
A7:
p <= b
by A5, XXREAL_1:1;
per cases
( p < b or p = b )
by A7, XXREAL_0:1;
suppose A8:
p < b
;
x in Cl Anow for r being Real st r > 0 holds
Ball (p,r) meets Alet r be
Real;
( r > 0 implies Ball (p,r) meets A )reconsider pp =
p + r as
Element of
RealSpace by METRIC_1:def 13, XREAL_0:def 1;
set pr =
min (
pp,
((p + b) / 2));
A9:
min (
pp,
((p + b) / 2))
<= (p + b) / 2
by XXREAL_0:17;
assume A10:
r > 0
;
Ball (p,r) meets A
p < min (
pp,
((p + b) / 2))
then consider Q being
irrational Real such that A11:
p < Q
and A12:
Q < min (
pp,
((p + b) / 2))
by Th26;
(p + b) / 2
< b
by A8, XREAL_1:226;
then
min (
pp,
((p + b) / 2))
< b
by A9, XXREAL_0:2;
then A13:
Q < b
by A12, XXREAL_0:2;
min (
pp,
((p + b) / 2))
<= pp
by XXREAL_0:17;
then A14:
(min (pp,((p + b) / 2))) - p <= pp - p
by XREAL_1:9;
reconsider P =
Q as
Element of
RealSpace by METRIC_1:def 13, XREAL_0:def 1;
P - p < (min (pp,((p + b) / 2))) - p
by A12, XREAL_1:9;
then
P - p < r
by A14, XXREAL_0:2;
then
dist (
p,
P)
< r
by A11, Th13;
then A15:
P in Ball (
p,
r)
by METRIC_1:11;
a < Q
by A6, A11, XXREAL_0:2;
then A16:
Q in ].a,b.[
by A13, XXREAL_1:4;
Q in IRRAT
by Th16;
then
Q in A
by A2, A16, XBOOLE_0:def 4;
hence
Ball (
p,
r)
meets A
by A15, XBOOLE_0:3;
verum end; hence
x in Cl A
by GOBOARD6:92, TOPMETR:def 6;
verum
end;