let C be Simple_closed_curve; :: thesis: for n being Element of NAT st n is_sufficiently_large_for C holds
UBD C misses BDD (L~ (Span (C,n)))
let n be Element of NAT ; :: thesis: ( n is_sufficiently_large_for C implies UBD C misses BDD (L~ (Span (C,n))) )
assume that
A1: n is_sufficiently_large_for C and
A2: UBD C meets BDD (L~ (Span (C,n))) ; :: thesis: contradiction
UBD (L~ (Span (C,n))) meets BDD (L~ (Span (C,n))) by A1, A2, Th15, XBOOLE_1:63;
hence contradiction by JORDAN2C:24; :: thesis: verum