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