let D be non empty compact non horizontal non vertical Subset of (TOP-REAL 2); for a being Real
for p being Point of (TOP-REAL 2) st a > 0 & p in L~ (SpStSeq D) holds
ex q being Point of (TOP-REAL 2) st
( q in UBD (L~ (SpStSeq D)) & |.(p - q).| < a )
let a be Real; for p being Point of (TOP-REAL 2) st a > 0 & p in L~ (SpStSeq D) holds
ex q being Point of (TOP-REAL 2) st
( q in UBD (L~ (SpStSeq D)) & |.(p - q).| < a )
let p be Point of (TOP-REAL 2); ( a > 0 & p in L~ (SpStSeq D) implies ex q being Point of (TOP-REAL 2) st
( q in UBD (L~ (SpStSeq D)) & |.(p - q).| < a ) )
assume that
A1:
a > 0
and
A2:
p in L~ (SpStSeq D)
; ex q being Point of (TOP-REAL 2) st
( q in UBD (L~ (SpStSeq D)) & |.(p - q).| < a )
set q1 = the Element of UBD (L~ (SpStSeq D));
set A = L~ (SpStSeq D);
(L~ (SpStSeq D)) ` <> {}
by SPRECT_1:def 3;
then consider A1, A2 being Subset of (TOP-REAL 2) such that
A3:
(L~ (SpStSeq D)) ` = A1 \/ A2
and
A1 misses A2
and
A4:
(Cl A1) \ A1 = (Cl A2) \ A2
and
A5:
L~ (SpStSeq D) = (Cl A1) \ A1
and
A6:
for C1, C2 being Subset of ((TOP-REAL 2) | ((L~ (SpStSeq D)) `)) st C1 = A1 & C2 = A2 holds
( C1 is a_component & C2 is a_component )
by Th82;
A7:
Down (A2,((L~ (SpStSeq D)) `)) = A2
by A3, XBOOLE_1:21;
UBD (L~ (SpStSeq D)) is_outside_component_of L~ (SpStSeq D)
by Th53;
then
UBD (L~ (SpStSeq D)) is_a_component_of (L~ (SpStSeq D)) `
;
then consider B1 being Subset of ((TOP-REAL 2) | ((L~ (SpStSeq D)) `)) such that
A8:
B1 = UBD (L~ (SpStSeq D))
and
A9:
B1 is a_component
by CONNSP_1:def 6;
B1 c= [#] ((TOP-REAL 2) | ((L~ (SpStSeq D)) `))
;
then A10:
UBD (L~ (SpStSeq D)) c= A1 \/ A2
by A3, A8, PRE_TOPC:def 5;
A11:
Down (A1,((L~ (SpStSeq D)) `)) = A1
by A3, XBOOLE_1:21;
then A12:
Down (A1,((L~ (SpStSeq D)) `)) is a_component
by A6, A7;
A13:
Down (A2,((L~ (SpStSeq D)) `)) is a_component
by A6, A11, A7;
A14:
UBD (L~ (SpStSeq D)) <> {}
by Th80;
then A15:
the Element of UBD (L~ (SpStSeq D)) in UBD (L~ (SpStSeq D))
;
per cases
( the Element of UBD (L~ (SpStSeq D)) in A1 or the Element of UBD (L~ (SpStSeq D)) in A2 )
by A10, A15, XBOOLE_0:def 3;
suppose
the
Element of
UBD (L~ (SpStSeq D)) in A1
;
ex q being Point of (TOP-REAL 2) st
( q in UBD (L~ (SpStSeq D)) & |.(p - q).| < a )then
B1 /\ (Down (A1,((L~ (SpStSeq D)) `))) <> {} ((TOP-REAL 2) | ((L~ (SpStSeq D)) `))
by A11, A8, A14, XBOOLE_0:def 4;
then
B1 meets Down (
A1,
((L~ (SpStSeq D)) `))
;
then
B1 = Down (
A1,
((L~ (SpStSeq D)) `))
by A12, A9, CONNSP_1:35;
then A16:
p in Cl (UBD (L~ (SpStSeq D)))
by A2, A5, A11, A8, XBOOLE_0:def 5;
reconsider ep =
p as
Point of
(Euclid 2) by TOPREAL3:8;
reconsider G2 =
Ball (
ep,
a) as
Subset of
(TOP-REAL 2) by TOPREAL3:8;
the
distance of
(Euclid 2) is
Reflexive
by METRIC_1:def 6;
then
dist (
ep,
ep)
= 0
;
then A17:
p in Ball (
ep,
a)
by A1, METRIC_1:11;
G2 is
open
by GOBOARD6:3;
then
UBD (L~ (SpStSeq D)) meets G2
by A16, A17, PRE_TOPC:def 7;
then consider t2 being
object such that A18:
t2 in UBD (L~ (SpStSeq D))
and A19:
t2 in G2
by XBOOLE_0:3;
reconsider qt2 =
t2 as
Point of
(TOP-REAL 2) by A18;
|.(p - qt2).| < a
by A19, Th87;
hence
ex
q being
Point of
(TOP-REAL 2) st
(
q in UBD (L~ (SpStSeq D)) &
|.(p - q).| < a )
by A18;
verum end; suppose
the
Element of
UBD (L~ (SpStSeq D)) in A2
;
ex q being Point of (TOP-REAL 2) st
( q in UBD (L~ (SpStSeq D)) & |.(p - q).| < a )then
B1 /\ (Down (A2,((L~ (SpStSeq D)) `))) <> {} ((TOP-REAL 2) | ((L~ (SpStSeq D)) `))
by A7, A8, A14, XBOOLE_0:def 4;
then
B1 meets Down (
A2,
((L~ (SpStSeq D)) `))
;
then
B1 = Down (
A2,
((L~ (SpStSeq D)) `))
by A13, A9, CONNSP_1:35;
then A20:
p in Cl (UBD (L~ (SpStSeq D)))
by A2, A4, A5, A7, A8, XBOOLE_0:def 5;
reconsider ep =
p as
Point of
(Euclid 2) by TOPREAL3:8;
reconsider G2 =
Ball (
ep,
a) as
Subset of
(TOP-REAL 2) by TOPREAL3:8;
the
distance of
(Euclid 2) is
Reflexive
by METRIC_1:def 6;
then
dist (
ep,
ep)
= 0
;
then A21:
p in Ball (
ep,
a)
by A1, METRIC_1:11;
G2 is
open
by GOBOARD6:3;
then
UBD (L~ (SpStSeq D)) meets G2
by A20, A21, PRE_TOPC:def 7;
then consider t2 being
object such that A22:
t2 in UBD (L~ (SpStSeq D))
and A23:
t2 in G2
by XBOOLE_0:3;
reconsider qt2 =
t2 as
Point of
(TOP-REAL 2) by A22;
|.(p - qt2).| < a
by A23, Th87;
hence
ex
q being
Point of
(TOP-REAL 2) st
(
q in UBD (L~ (SpStSeq D)) &
|.(p - q).| < a )
by A22;
verum end;