let C be Simple_closed_curve; :: thesis: for n being Nat st n is_sufficiently_large_for C holds
BDD (L~ (Span (C,n))) c= BDD C
let n be Nat; :: thesis: ( n is_sufficiently_large_for C implies BDD (L~ (Span (C,n))) c= BDD C )
assume that
A1: n is_sufficiently_large_for C and
A2: not BDD (L~ (Span (C,n))) c= BDD C ; :: thesis: contradiction
set f = Span (C,n);
A3: Cl (BDD (L~ (Span (C,n)))) = Cl (RightComp (Span (C,n))) by GOBRD14:37
.= (RightComp (Span (C,n))) \/ (L~ (Span (C,n))) by GOBRD14:21 ;
len (Span (C,n)) >= 1 by GOBOARD7:34, XXREAL_0:2;
then A4: 1 in dom (Span (C,n)) by FINSEQ_3:25;
len (Span (C,n)) > 4 by GOBOARD7:34;
then (Span (C,n)) /. 1 in L~ (Span (C,n)) by A4, GOBOARD1:1, XXREAL_0:2;
then SpanStart (C,n) in L~ (Span (C,n)) by A1, JORDAN13:def 1;
then A5: SpanStart (C,n) in Cl (BDD (L~ (Span (C,n)))) by A3, XBOOLE_0:def 3;
SpanStart (C,n) in BDD C by A1, Th6;
then A6: BDD (L~ (Span (C,n))) meets BDD C by A5, PRE_TOPC:def 7;
BDD C misses UBD C by JORDAN2C:24;
then A7: BDD C, UBD C are_separated by TSEP_1:37;
BDD (L~ (Span (C,n))) misses UBD (L~ (Span (C,n))) by JORDAN2C:24;
then C misses BDD (L~ (Span (C,n))) by A1, Th12, XBOOLE_1:63;
then A8: BDD (L~ (Span (C,n))) c= C ` by SUBSET_1:23;
(BDD C) \/ (UBD C) = C ` by JORDAN2C:27;
then BDD (L~ (Span (C,n))) c= UBD C by A2, A8, A7, CONNSP_1:16;
then BDD C meets UBD C by A6, XBOOLE_1:63;
hence contradiction by JORDAN2C:24; :: thesis: verum