let C be Simple_closed_curve; :: thesis: for n being Nat st n is_sufficiently_large_for C holds
UBD C c= UBD (L~ (Span (C,n)))
let n be 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)))
let x be object ; :: according to TARSKI:def 3 :: thesis: ( 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 ; :: thesis: 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;
A5: now :: thesis: not x in L~ (Span (C,n))
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:21;
then p in Cl (BDD (L~ (Span (C,n)))) by GOBRD14:37;
hence contradiction by A4, A2, A3, PRE_TOPC:def 7; :: thesis: verum
end;
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; :: thesis: verum