let D be non empty compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: 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; :: thesis: 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); :: thesis: ( 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 A1:
( a > 0 & p in L~ (SpStSeq D) )
; :: thesis: ex q being Point of (TOP-REAL 2) st
( q in UBD (L~ (SpStSeq D)) & |.(p - q).| < a )
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
A2:
( (L~ (SpStSeq D)) ` = A1 \/ A2 & A1 misses A2 & (Cl A1) \ A1 = (Cl A2) \ A2 & L~ (SpStSeq D) = (Cl A1) \ A1 & ( for C1, C2 being Subset of ((TOP-REAL 2) | ((L~ (SpStSeq D)) ` )) st C1 = A1 & C2 = A2 holds
( C1 is_a_component_of (TOP-REAL 2) | ((L~ (SpStSeq D)) ` ) & C2 is_a_component_of (TOP-REAL 2) | ((L~ (SpStSeq D)) ` ) ) ) )
by Th106;
A3:
Down A1,((L~ (SpStSeq D)) ` ) = A1
by A2, XBOOLE_1:21;
A4:
Down A2,((L~ (SpStSeq D)) ` ) = A2
by A2, XBOOLE_1:21;
then A5:
( Down A1,((L~ (SpStSeq D)) ` ) is_a_component_of (TOP-REAL 2) | ((L~ (SpStSeq D)) ` ) & Down A2,((L~ (SpStSeq D)) ` ) is_a_component_of (TOP-REAL 2) | ((L~ (SpStSeq D)) ` ) )
by A2, A3;
UBD (L~ (SpStSeq D)) is_outside_component_of L~ (SpStSeq D)
by Th76;
then
UBD (L~ (SpStSeq D)) is_a_component_of (L~ (SpStSeq D)) `
by Def4;
then consider B1 being Subset of ((TOP-REAL 2) | ((L~ (SpStSeq D)) ` )) such that
A6:
( B1 = UBD (L~ (SpStSeq D)) & B1 is_a_component_of (TOP-REAL 2) | ((L~ (SpStSeq D)) ` ) )
by CONNSP_1:def 6;
B1 c= [#] ((TOP-REAL 2) | ((L~ (SpStSeq D)) ` ))
;
then A7:
UBD (L~ (SpStSeq D)) c= A1 \/ A2
by A2, A6, PRE_TOPC:def 10;
consider q1 being Element of UBD (L~ (SpStSeq D));
A8:
UBD (L~ (SpStSeq D)) <> {}
by Th104;
then A9:
q1 in UBD (L~ (SpStSeq D))
;
per cases
( q1 in A1 or q1 in A2 )
by A7, A9, XBOOLE_0:def 3;
suppose
q1 in A1
;
:: thesis: 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 A3, A6, A8, XBOOLE_0:def 4;
then
B1 meets Down A1,
((L~ (SpStSeq D)) ` )
by XBOOLE_0:def 7;
then
B1 = Down A1,
((L~ (SpStSeq D)) ` )
by A5, A6, CONNSP_1:37;
then A10:
p in Cl (UBD (L~ (SpStSeq D)))
by A1, A2, A3, A6, XBOOLE_0:def 5;
reconsider ep =
p as
Point of
(Euclid 2) by TOPREAL3:13;
reconsider G2 =
Ball ep,
a as
Subset of
(TOP-REAL 2) by TOPREAL3:13;
the
distance of
(Euclid 2) is
Reflexive
by METRIC_1:def 7;
then
the
distance of
(Euclid 2) . ep,
ep = 0
by METRIC_1:def 3;
then
dist ep,
ep = 0
by METRIC_1:def 1;
then A11:
p in Ball ep,
a
by A1, METRIC_1:12;
G2 is
open
by GOBOARD6:6;
then
UBD (L~ (SpStSeq D)) meets G2
by A10, A11, PRE_TOPC:def 13;
then consider t2 being
set such that A12:
(
t2 in UBD (L~ (SpStSeq D)) &
t2 in G2 )
by XBOOLE_0:3;
reconsider qt2 =
t2 as
Point of
(TOP-REAL 2) by A12;
(
t2 in UBD (L~ (SpStSeq D)) &
|.(p - qt2).| < a )
by A12, Th111;
hence
ex
q being
Point of
(TOP-REAL 2) st
(
q in UBD (L~ (SpStSeq D)) &
|.(p - q).| < a )
;
:: thesis: verum end; suppose
q1 in A2
;
:: thesis: 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 A4, A6, A8, XBOOLE_0:def 4;
then
B1 meets Down A2,
((L~ (SpStSeq D)) ` )
by XBOOLE_0:def 7;
then
B1 = Down A2,
((L~ (SpStSeq D)) ` )
by A5, A6, CONNSP_1:37;
then A13:
p in Cl (UBD (L~ (SpStSeq D)))
by A1, A2, A4, A6, XBOOLE_0:def 5;
reconsider ep =
p as
Point of
(Euclid 2) by TOPREAL3:13;
reconsider G2 =
Ball ep,
a as
Subset of
(TOP-REAL 2) by TOPREAL3:13;
the
distance of
(Euclid 2) is
Reflexive
by METRIC_1:def 7;
then
the
distance of
(Euclid 2) . ep,
ep = 0
by METRIC_1:def 3;
then
dist ep,
ep = 0
by METRIC_1:def 1;
then A14:
p in Ball ep,
a
by A1, METRIC_1:12;
G2 is
open
by GOBOARD6:6;
then
UBD (L~ (SpStSeq D)) meets G2
by A13, A14, PRE_TOPC:def 13;
then consider t2 being
set such that A15:
(
t2 in UBD (L~ (SpStSeq D)) &
t2 in G2 )
by XBOOLE_0:3;
reconsider qt2 =
t2 as
Point of
(TOP-REAL 2) by A15;
(
t2 in UBD (L~ (SpStSeq D)) &
|.(p - qt2).| < a )
by A15, Th111;
hence
ex
q being
Point of
(TOP-REAL 2) st
(
q in UBD (L~ (SpStSeq D)) &
|.(p - q).| < a )
;
:: thesis: verum end;