let n be 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))
assume not BDD C misses L~ (Cage (C,n)) ; :: thesis: contradiction
then consider x being object such that
A1: x in (BDD C) /\ (L~ (Cage (C,n))) by XBOOLE_0:4;
A2: x in L~ (Cage (C,n)) by A1, XBOOLE_0:def 4;
( BDD C = union { B where B is Subset of (TOP-REAL 2) : B is_inside_component_of C } & x in BDD C ) by A1, JORDAN2C:def 4, XBOOLE_0:def 4;
then consider Z being set such that
A3: x in Z and
A4: Z in { B where B is Subset of (TOP-REAL 2) : B is_inside_component_of C } by TARSKI:def 4;
consider B being Subset of (TOP-REAL 2) such that
A5: Z = B and
A6: B is_inside_component_of C by A4;
B misses L~ (Cage (C,n)) by A6, Th18;
then B /\ (L~ (Cage (C,n))) = {} ;
hence contradiction by A3, A5, A2, XBOOLE_0:def 4; :: thesis: verum