let n be Element of NAT ; :: thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds BDD C misses L~ (Cage C,n)
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: BDD C misses L~ (Cage C,n)
A1: BDD C = union { B where B is Subset of (TOP-REAL 2) : B is_inside_component_of C } by JORDAN2C:def 5;
assume not BDD C misses L~ (Cage C,n) ; :: thesis: contradiction
then consider x being set such that
A2: x in (BDD C) /\ (L~ (Cage C,n)) by XBOOLE_0:4;
x in BDD C by A2, XBOOLE_0:def 4;
then consider Z being set such that
A3: ( x in Z & Z in { B where B is Subset of (TOP-REAL 2) : B is_inside_component_of C } ) by A1, TARSKI:def 4;
consider B being Subset of (TOP-REAL 2) such that
A4: ( Z = B & B is_inside_component_of C ) by A3;
B misses L~ (Cage C,n) by A4, Th18;
then A5: B /\ (L~ (Cage C,n)) = {} by XBOOLE_0:def 7;
x in L~ (Cage C,n) by A2, XBOOLE_0:def 4;
hence contradiction by A3, A4, A5, XBOOLE_0:def 4; :: thesis: verum