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: 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 ;
len (Span C,n) >= 1 by GOBOARD7:36, XXREAL_0:2;
then A4: 1 in dom (Span C,n) by FINSEQ_3:27;
len (Span C,n) > 4 by GOBOARD7:36;
then (Span C,n) /. 1 in L~ (Span C,n) by A4, GOBOARD1:16, 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, Th7;
then A6: BDD (L~ (Span C,n)) meets BDD C by A5, PRE_TOPC:def 13;
BDD C misses UBD C by JORDAN2C:28;
then A7: BDD C, UBD C are_separated by TSEP_1:41;
BDD (L~ (Span C,n)) misses UBD (L~ (Span C,n)) by JORDAN2C:28;
then C misses BDD (L~ (Span C,n)) by A1, Th13, XBOOLE_1:63;
then A8: BDD (L~ (Span C,n)) c= C ` by SUBSET_1:43;
(BDD C) \/ (UBD C) = C ` by JORDAN2C:31;
then BDD (L~ (Span C,n)) c= UBD C by A2, A8, A7, CONNSP_1:17;
then BDD C meets UBD C by A6, XBOOLE_1:63;
hence contradiction by JORDAN2C:28; :: thesis: verum