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))
A1: C c= RightComp (Cage C,n) by Th11;
RightComp (Cage C,n) c= BDD (L~ (Cage C,n)) by GOBRD14:45, JORDAN2C:26;
hence C c= BDD (L~ (Cage C,n)) by A1, XBOOLE_1:1; :: thesis: verum