for C being Simple_closed_curve
for i being Nat holds Fr ((UBD (L~ (Cage (C,i)))) `) = L~ (Cage (C,i))