let C be Simple_closed_curve; :: thesis: for n being Element of NAT st n is_sufficiently_large_for C holds
C c= UBD (L~ (Span C,n))
let n be Element of 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 Th12;
LeftComp (Span C,n) c= UBD (L~ (Span C,n)) by GOBRD14:44, JORDAN2C:27;
hence C c= UBD (L~ (Span C,n)) by A1, XBOOLE_1:1; :: thesis: verum