let n be 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:22;
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:4;
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:18; :: thesis: verum