let A be Subset of R^1; :: thesis: for a, b being Real st a < b & A = RAT (a,b) holds
Cl A = [.a,b.]
let a, b be Real; :: thesis: ( a < b & A = RAT (a,b) implies Cl A = [.a,b.] )
assume that
A1: a < b and
A2: A = RAT (a,b) ; :: thesis: Cl A = [.a,b.]
reconsider ab = ].a,b.[, RT = RAT as Subset of R^1 by NUMBERS:12, TOPMETR:17;
reconsider RR = RAT /\ ].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.] :: according to XBOOLE_0:def 10 :: thesis: [.a,b.] c= Cl A

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Cl A or x in [.a,b.] )
assume x in Cl A ; :: thesis: x in [.a,b.]
then x in (Cl RT) /\ (Cl ab) by A2, A4;
then x in the carrier of R^1 /\ (Cl ab) by Th14;
hence x in [.a,b.] by A1, A3, Th15; :: thesis: verum

end;

thus [.a,b.] c= Cl A :: thesis: verum

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in [.a,b.] or x in Cl A )
assume A5: x in [.a,b.] ; :: thesis: 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 ; :: thesis: x in Cl A

now :: thesis: for r being Real st r > 0 holds
Ball (p,r) meets A

let r be Real; :: thesis: ( 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 ; :: thesis: Ball (p,r) meets A
p < min (pp,((p + b) / 2))

proof

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

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

hence p < min (pp,((p + b) / 2)) by A10, XREAL_1:29; :: thesis: verum

end;

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

hence p < min (pp,((p + b) / 2)) by A8, XREAL_1:226; :: thesis: verum

end;

end;

end;

then consider Q being Rational such that
A11: p < Q and
A12: Q < min (pp,((p + b) / 2)) by RAT_1:7;
(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 RAT by RAT_1:def 2;
then Q in A by A2, A16, XBOOLE_0:def 4;
hence Ball (p,r) meets A by A15, XBOOLE_0:3; :: thesis: verum

end;

hence x in Cl A by GOBOARD6:92, TOPMETR:def 6; :: thesis: verum

end;

suppose p = b ; :: thesis: x in Cl A

hence x in Cl A by A1, A2, Lm2; :: thesis: verum

end;

end;

end;