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:28; :: thesis: verum