let n be 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