let C be Simple_closed_curve; :: thesis: for n being Nat st n is_sufficiently_large_for C holds
UBD C c= LeftComp (Span (C,n))
let n be Nat; :: thesis: ( n is_sufficiently_large_for C implies UBD C c= LeftComp (Span (C,n)) )
assume n is_sufficiently_large_for C ; :: thesis: UBD C c= LeftComp (Span (C,n))
then UBD C c= UBD (L~ (Span (C,n))) by Th14;
hence UBD C c= LeftComp (Span (C,n)) by GOBRD14:36; :: thesis: verum