let n be Element of NAT ; :: thesis: for C being being_simple_closed_curve Subset of (TOP-REAL 2) holds L~ (Cage C,n) c= UBD C
let C be being_simple_closed_curve Subset of (TOP-REAL 2); :: thesis: L~ (Cage C,n) c= UBD C
C c= BDD (L~ (Cage C,n)) by JORDAN10:12;
hence L~ (Cage C,n) c= UBD C by Th16; :: thesis: verum