let A be Subset of R^1 ; :: thesis: ( A = RAT implies Cl A = the carrier of R^1 )
assume A1:
A = RAT
; :: thesis: Cl A = the carrier of R^1
Cl A = the carrier of R^1
proof
thus
Cl A c= the
carrier of
R^1
;
:: according to XBOOLE_0:def 10 :: thesis: the carrier of R^1 c= Cl A
thus
the
carrier of
R^1 c= Cl A
:: thesis: verumproof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in the carrier of R^1 or x in Cl A )
assume
x in the
carrier of
R^1
;
:: thesis: x in Cl A
then reconsider p =
x as
Element of
RealSpace by METRIC_1:def 14, TOPMETR:24;
now let r be
real number ;
:: thesis: ( r > 0 implies Ball p,r meets A )assume A2:
r > 0
;
:: thesis: Ball p,r meets Areconsider pr =
p + r as
Element of
RealSpace by METRIC_1:def 14, XREAL_0:def 1;
p < pr
by A2, XREAL_1:31;
then consider Q being
rational number such that A3:
(
p < Q &
Q < pr )
by RAT_1:22;
A4:
Q in A
by A1, RAT_1:def 2;
reconsider P =
Q as
Element of
RealSpace by METRIC_1:def 14, XREAL_0:def 1;
P - p < pr - p
by A3, XREAL_1:11;
then
dist p,
P < r
by A3, Th34;
then
P in Ball p,
r
by METRIC_1:12;
hence
Ball p,
r meets A
by A4, XBOOLE_0:3;
:: thesis: verum end;
hence
x in Cl A
by GOBOARD6:95, TOPMETR:def 7;
:: thesis: verum
end;
end;
hence
Cl A = the carrier of R^1
; :: thesis: verum