let n be Nat; for P, P1, Q being Subset of (TOP-REAL n)
for W being Subset of (Euclid n) st P = W & P is connected & not W is bounded & P1 = Component_of (Down (P,(Q `))) & W misses Q holds
P1 is_outside_component_of Q
let P, P1 be Subset of (TOP-REAL n); for Q being Subset of (TOP-REAL n)
for W being Subset of (Euclid n) st P = W & P is connected & not W is bounded & P1 = Component_of (Down (P,(Q `))) & W misses Q holds
P1 is_outside_component_of Q
let Q be Subset of (TOP-REAL n); for W being Subset of (Euclid n) st P = W & P is connected & not W is bounded & P1 = Component_of (Down (P,(Q `))) & W misses Q holds
P1 is_outside_component_of Q
let W be Subset of (Euclid n); ( P = W & P is connected & not W is bounded & P1 = Component_of (Down (P,(Q `))) & W misses Q implies P1 is_outside_component_of Q )
assume that
A1:
P = W
and
A2:
P is connected
and
A3:
not W is bounded
and
A4:
P1 = Component_of (Down (P,(Q `)))
and
A5:
W misses Q
; P1 is_outside_component_of Q
A6:
(TOP-REAL n) | P is connected
by A2, CONNSP_1:def 3;
A7: Down (P,(Q `)) =
P \ Q
by SUBSET_1:13
.=
P
by A1, A5, XBOOLE_1:83
;
then reconsider P0 = P as Subset of ((TOP-REAL n) | (Q `)) ;
reconsider W0 = Component_of P0 as Subset of (Euclid n) by A4, A7, TOPREAL3:8;
P0 c= Q `
by A1, A5, SUBSET_1:23;
then
((TOP-REAL n) | (Q `)) | P0 = (TOP-REAL n) | P
by PRE_TOPC:7;
then A8:
P0 is connected
by A6, CONNSP_1:def 3;
A10:
W <> {} (Euclid n)
by A3;
A11:
W /\ Q = {}
by A5;
then reconsider Q1 = Q ` as non empty Subset of (TOP-REAL n) ;
not (TOP-REAL n) | Q1 is empty
;
then
Component_of P0 is a_component
by A1, A10, A8, CONNSP_3:9;
hence
P1 is_outside_component_of Q
by A4, A7, A9, Th8; verum