let C be Simple_closed_curve; :: thesis: for n being Element of NAT st n is_sufficiently_large_for C holds
UBD C c= UBD (L~ (Span C,n))
let n be Element of NAT ; :: thesis: ( n is_sufficiently_large_for C implies UBD C c= UBD (L~ (Span C,n)) )
assume A1: n is_sufficiently_large_for C ; :: thesis: UBD C c= UBD (L~ (Span C,n))
then A2: BDD (L~ (Span C,n)) c= BDD C by Th14;
A3: Cl (BDD (L~ (Span C,n))) c= Cl (BDD C) by A1, Th14, PRE_TOPC:49;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in UBD C or x in UBD (L~ (Span C,n)) )
A4: BDD C misses UBD C by JORDAN2C:28;
assume A5: x in UBD C ; :: thesis: x in UBD (L~ (Span C,n))
then reconsider p = x as Point of (TOP-REAL 2) ;
not x in BDD (L~ (Span C,n)) by A2, A4, A5, XBOOLE_0:3;
then A6: not x in RightComp (Span C,n) by GOBRD14:47;

now

assume x in L~ (Span C,n) ; :: thesis: contradiction
then p in (RightComp (Span C,n)) \/ (L~ (Span C,n)) by XBOOLE_0:def 3;
then p in Cl (RightComp (Span C,n)) by GOBRD14:31;
then p in Cl (BDD (L~ (Span C,n))) by GOBRD14:47;
hence contradiction by A3, A4, A5, PRE_TOPC:def 13; :: thesis: verum

end;

then p in LeftComp (Span C,n) by A6, GOBRD14:27;
hence x in UBD (L~ (Span C,n)) by GOBRD14:46; :: thesis: verum