let C be Simple_closed_curve; :: thesis: for n being Nat st n is_sufficiently_large_for C holds
L~ (Span (C,n)) c= BDD C
let n be 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 C misses L~ (Span (C,n)) by Th8;
then L~ (Span (C,n)) c= C ` by SUBSET_1:23;
then A2: L~ (Span (C,n)) c= (BDD C) \/ (UBD C) by JORDAN2C:27;
UBD C misses L~ (Span (C,n)) by A1, Th20;
hence L~ (Span (C,n)) c= BDD C by A2, XBOOLE_1:73; :: thesis: verum