let C be Simple_closed_curve; :: thesis: for n being Element of NAT st n is_sufficiently_large_for C holds
L~ (Span C,n) c= BDD C
let n be Element of NAT ; :: thesis: ( n is_sufficiently_large_for C implies L~ (Span C,n) c= BDD C )
assume A1: n is_sufficiently_large_for C ; :: thesis: L~ (Span C,n) c= BDD C
then A2: UBD C misses L~ (Span C,n) by Th21;
C misses L~ (Span C,n) by A1, Th9;
then L~ (Span C,n) c= C ` by SUBSET_1:43;
then L~ (Span C,n) c= (BDD C) \/ (UBD C) by JORDAN2C:31;
hence L~ (Span C,n) c= BDD C by A2, XBOOLE_1:73; :: thesis: verum