let C be Simple_closed_curve; for n being Nat st n is_sufficiently_large_for C holds
UBD C c= UBD (L~ (Span (C,n)))
let n be Nat; ( n is_sufficiently_large_for C implies UBD C c= UBD (L~ (Span (C,n))) )
assume A1:
n is_sufficiently_large_for C
; UBD C c= UBD (L~ (Span (C,n)))
let x be object ; TARSKI:def 3 ( not x in UBD C or x in UBD (L~ (Span (C,n))) )
A2:
BDD C misses UBD C
by JORDAN2C:24;
assume A3:
x in UBD C
; x in UBD (L~ (Span (C,n)))
then reconsider p = x as Point of (TOP-REAL 2) ;
A4:
Cl (BDD (L~ (Span (C,n)))) c= Cl (BDD C)
by A1, Th13, PRE_TOPC:19;
BDD (L~ (Span (C,n))) c= BDD C
by A1, Th13;
then
not x in BDD (L~ (Span (C,n)))
by A2, A3, XBOOLE_0:3;
then
not x in RightComp (Span (C,n))
by GOBRD14:37;
then
p in LeftComp (Span (C,n))
by A5, GOBRD14:17;
hence
x in UBD (L~ (Span (C,n)))
by GOBRD14:36; verum