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