let n be Element of NAT ; :: thesis: for P being Subset of (TOP-REAL 2)
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st P is_inside_component_of C holds
P misses L~ (Cage C,n)
let P be Subset of (TOP-REAL 2); :: thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st P is_inside_component_of C holds
P misses L~ (Cage C,n)
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: ( P is_inside_component_of C implies P misses L~ (Cage C,n) )
set f = Cage C,n;
assume P is_inside_component_of C ; :: thesis: P misses L~ (Cage C,n)
then A1: P c= BDD C by JORDAN2C:26;
assume P /\ (L~ (Cage C,n)) <> {} ; :: according to XBOOLE_0:def 7 :: thesis: contradiction
then consider x being Point of (TOP-REAL 2) such that
A2: x in P /\ (L~ (Cage C,n)) by SUBSET_1:10;
x in P by A2, XBOOLE_0:def 4;
then A3: x in BDD C by A1;
A4: BDD C c= RightComp (Cage C,n) by Th17;
x in L~ (Cage C,n) by A2, XBOOLE_0:def 4;
hence contradiction by A3, A4, GOBRD14:28; :: thesis: verum