let X be Subset of REAL; ( X in Family_open_set RealSpace implies X is open )
assume A1:
X in Family_open_set RealSpace
; X is open
for r being Element of REAL st r in X holds
ex N being Neighbourhood of r st N c= X
proof
let r be
Element of
REAL ;
( r in X implies ex N being Neighbourhood of r st N c= X )
assume A2:
r in X
;
ex N being Neighbourhood of r st N c= X
reconsider r =
r as
Element of
REAL ;
reconsider x =
r as
Element of
RealSpace by METRIC_1:def 13;
ex
N being
Neighbourhood of
r st
N c= X
proof
consider r1 being
Real such that A3:
r1 > 0
and A4:
Ball (
x,
r1)
c= X
by A1, A2, PCOMPS_1:def 4;
reconsider N1 =
Ball (
x,
r1) as
Subset of
REAL by METRIC_1:def 13;
ex
g being
Real st
(
0 < g &
Ball (
x,
r1)
= ].(r - g),(r + g).[ )
proof
take g =
r1;
( 0 < g & Ball (x,r1) = ].(r - g),(r + g).[ )
A5:
].(r - g),(r + g).[ c= N1
proof
let a be
object ;
TARSKI:def 3 ( not a in ].(r - g),(r + g).[ or a in N1 )
assume A6:
a in ].(r - g),(r + g).[
;
a in N1
then reconsider a9 =
a as
Element of
REAL ;
a9 is
Element of
REAL
;
then reconsider a99 =
a,
r9 =
r as
Element of
RealSpace by METRIC_1:def 13;
reconsider a1 =
a9,
r1 =
r9 as
Element of
REAL ;
|.(a9 - r).| < g
by A6, RCOMP_1:1;
then
real_dist . (
a9,
r)
< g
by METRIC_1:def 12;
then
(
dist (
r9,
a99)
= real_dist . (
r,
a9) &
real_dist . (
r1,
a1)
< g )
by METRIC_1:9, METRIC_1:def 1, METRIC_1:def 13;
hence
a in N1
by METRIC_1:11;
verum
end;
N1 c= ].(r - g),(r + g).[
proof
let a be
object ;
TARSKI:def 3 ( not a in N1 or a in ].(r - g),(r + g).[ )
assume
a in N1
;
a in ].(r - g),(r + g).[
then
a in { q where q is Element of RealSpace : dist (x,q) < g }
by METRIC_1:17;
then consider q being
Element of
RealSpace such that A7:
q = a
and A8:
dist (
x,
q)
< g
;
reconsider a9 =
a as
Real by A7;
reconsider x1 =
x,
q1 =
q as
Element of
REAL by METRIC_1:def 13;
real_dist . (
q1,
x1)
< g
by A8, METRIC_1:def 1, METRIC_1:def 13;
then
|.(a9 - r).| < g
by A7, METRIC_1:def 12;
hence
a in ].(r - g),(r + g).[
by RCOMP_1:1;
verum
end;
hence
(
0 < g &
Ball (
x,
r1)
= ].(r - g),(r + g).[ )
by A3, A5;
verum
end;
then reconsider N =
N1 as
Neighbourhood of
r by RCOMP_1:def 6;
take
N
;
N c= X
thus
N c= X
by A4;
verum
end;
hence
ex
N being
Neighbourhood of
r st
N c= X
;
verum
end;
hence
X is open
by RCOMP_1:20; verum