let n be Element of 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:45, JORDAN2C:26;
hence C c= BDD (L~ (Cage (C,n))) by XBOOLE_1:1; :: thesis: verum