let n be Nat; :: thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds C c= BDD (L~ (Cage (C,n)))
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: C c= BDD (L~ (Cage (C,n)))
( C c= RightComp (Cage (C,n)) & RightComp (Cage (C,n)) c= BDD (L~ (Cage (C,n))) ) by Th11, GOBRD14:35, JORDAN2C:22;
hence C c= BDD (L~ (Cage (C,n))) ; :: thesis: verum