let C be Simple_closed_curve; :: thesis: for n being Element of NAT st n is_sufficiently_large_for C holds
UBD C c= LeftComp (Span C,n)
let n be Element of 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 Th15;
hence UBD C c= LeftComp (Span C,n) by GOBRD14:46; :: thesis: verum