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

proof

let x be set ; :: 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 Th51;
hence x in [.a,b.] by A1, A3, Th36; :: thesis: verum

end;

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

proof

let x be set ; :: 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 14;
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

let r be real number ; :: thesis: ( r > 0 implies Ball p,r meets A )
reconsider pp = p + r as Element of RealSpace by METRIC_1:def 14, 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:31; :: 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:228; :: thesis: verum

end;

end;

end;

then consider Q being real irrational number such that
A11: p < Q and
A12: Q < min pp,((p + b) / 2) by Th50;
(p + b) / 2 < b by A8, XREAL_1:228;
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:11;
reconsider P = Q as Element of RealSpace by METRIC_1:def 14, XREAL_0:def 1;
P - p < (min pp,((p + b) / 2)) - p by A12, XREAL_1:11;
then P - p < r by A14, XXREAL_0:2;
then dist p,P < r by A11, Th34;
then A15: P in Ball p,r by METRIC_1:12;
a < Q by A6, A11, XXREAL_0:2;
then A16: Q in ].a,b.[ by A13, XXREAL_1:4;
Q in IRRAT by Th37;
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:95, TOPMETR:def 7; :: thesis: verum

end;

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

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

end;

end;

end;