let C be Simple_closed_curve; :: thesis: for n being Element of NAT st n is_sufficiently_large_for C holds
BDD (L~ (Span C,n)) c= BDD C
let n be Element of 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: SpanStart C,n in BDD C by A1, Th7;
A4: Cl (BDD (L~ (Span C,n))) = Cl (RightComp (Span C,n)) by GOBRD14:47
.= (RightComp (Span C,n)) \/ (L~ (Span C,n)) by GOBRD14:31 ;
A5: len (Span C,n) > 4 by GOBOARD7:36;
( len (Span C,n) >= 2 & len (Span C,n) >= 1 ) by GOBOARD7:36, XXREAL_0:2;
then 1 in dom (Span C,n) by FINSEQ_3:27;
then (Span C,n) /. 1 in L~ (Span C,n) by A5, GOBOARD1:16, XXREAL_0:2;
then SpanStart C,n in L~ (Span C,n) by A1, JORDAN13:def 1;
then SpanStart C,n in Cl (BDD (L~ (Span C,n))) by A4, XBOOLE_0:def 3;
then A6: BDD (L~ (Span C,n)) meets BDD C by A3, PRE_TOPC:def 13;
A7: BDD (L~ (Span C,n)) misses UBD (L~ (Span C,n)) by JORDAN2C:28;
A8: (BDD C) \/ (UBD C) = C ` by JORDAN2C:31;
C misses BDD (L~ (Span C,n)) by A1, A7, Th13, XBOOLE_1:63;
then A9: BDD (L~ (Span C,n)) c= C ` by SUBSET_1:43;
BDD C misses UBD C by JORDAN2C:28;
then BDD C, UBD C are_separated by TSEP_1:41;
then BDD (L~ (Span C,n)) c= UBD C by A2, A8, A9, CONNSP_1:17;
then BDD C meets UBD C by A6, XBOOLE_1:63;
hence contradiction by JORDAN2C:28; :: thesis: verum