:: JORDAN11 semantic presentation

begin

definition
let C be ( ( being_simple_closed_curve ) ( non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() ) Subset of ) ;
func ApproxIndex C -> ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) means :: JORDAN11:def 1
( it : ( ( ) ( ) Element of C : ( ( ) ( ) RLTopStruct ) ) is_sufficiently_large_for C : ( ( ) ( ) RLTopStruct ) & ( for j being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) st j : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) is_sufficiently_large_for C : ( ( ) ( ) RLTopStruct ) holds
j : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) >= it : ( ( ) ( ) Element of C : ( ( ) ( ) RLTopStruct ) ) ) );
end;

theorem :: JORDAN11:1
for C being ( ( being_simple_closed_curve ) ( non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() ) Subset of ) holds ApproxIndex C : ( ( being_simple_closed_curve ) ( non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() ) Subset of ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) >= 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ;

definition
let C be ( ( being_simple_closed_curve ) ( non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() ) Subset of ) ;
func Y-InitStart C -> ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) means :: JORDAN11:def 2
( it : ( ( ) ( ) Element of C : ( ( ) ( ) RLTopStruct ) ) < width (Gauge (C : ( ( ) ( ) RLTopStruct ) ,(ApproxIndex C : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( tabular ) ( V21() V24( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) V25(K292( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V153() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V29() ) set ) ) : ( ( ) ( ) M9( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V153() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V29() ) set ) )) ) V26() FinSequence-like tabular ) FinSequence of K292( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V153() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V29() ) set ) ) : ( ( ) ( ) M9( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V153() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V29() ) set ) )) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) & cell ((Gauge (C : ( ( ) ( ) RLTopStruct ) ,(ApproxIndex C : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( tabular ) ( V21() V24( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) V25(K292( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V153() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V29() ) set ) ) : ( ( ) ( ) M9( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V153() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V29() ) set ) )) ) V26() FinSequence-like tabular ) FinSequence of K292( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V153() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V29() ) set ) ) : ( ( ) ( ) M9( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V153() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V29() ) set ) )) ) ,((X-SpanStart (C : ( ( ) ( ) RLTopStruct ) ,(ApproxIndex C : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) -' 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,it : ( ( ) ( ) Element of C : ( ( ) ( ) RLTopStruct ) ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V153() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V29() ) set ) ) : ( ( ) ( non empty ) set ) ) c= BDD C : ( ( ) ( ) RLTopStruct ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V153() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V29() ) set ) ) : ( ( ) ( non empty ) set ) ) & ( for j being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) st j : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) < width (Gauge (C : ( ( ) ( ) RLTopStruct ) ,(ApproxIndex C : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( tabular ) ( V21() V24( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) V25(K292( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V153() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V29() ) set ) ) : ( ( ) ( ) M9( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V153() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V29() ) set ) )) ) V26() FinSequence-like tabular ) FinSequence of K292( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V153() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V29() ) set ) ) : ( ( ) ( ) M9( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V153() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V29() ) set ) )) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) & cell ((Gauge (C : ( ( ) ( ) RLTopStruct ) ,(ApproxIndex C : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( tabular ) ( V21() V24( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) V25(K292( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V153() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V29() ) set ) ) : ( ( ) ( ) M9( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V153() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V29() ) set ) )) ) V26() FinSequence-like tabular ) FinSequence of K292( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V153() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V29() ) set ) ) : ( ( ) ( ) M9( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V153() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V29() ) set ) )) ) ,((X-SpanStart (C : ( ( ) ( ) RLTopStruct ) ,(ApproxIndex C : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) -' 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,j : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V153() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V29() ) set ) ) : ( ( ) ( non empty ) set ) ) c= BDD C : ( ( ) ( ) RLTopStruct ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V153() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V29() ) set ) ) : ( ( ) ( non empty ) set ) ) holds
j : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) >= it : ( ( ) ( ) Element of C : ( ( ) ( ) RLTopStruct ) ) ) );
end;

theorem :: JORDAN11:2
for C being ( ( being_simple_closed_curve ) ( non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() ) Subset of ) holds Y-InitStart C : ( ( being_simple_closed_curve ) ( non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() ) Subset of ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) > 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: JORDAN11:3
for C being ( ( being_simple_closed_curve ) ( non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() ) Subset of ) holds (Y-InitStart C : ( ( being_simple_closed_curve ) ( non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() ) Subset of ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) < width (Gauge (C : ( ( being_simple_closed_curve ) ( non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() ) Subset of ) ,(ApproxIndex C : ( ( being_simple_closed_curve ) ( non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() ) Subset of ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( tabular ) ( V21() V23() V24( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) V25(K292( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V153() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V29() ) set ) ) : ( ( ) ( ) M9( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V153() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V29() ) set ) )) ) V26() FinSequence-like tabular V257() V258() V259() V260() ) FinSequence of K292( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V153() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V29() ) set ) ) : ( ( ) ( ) M9( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V153() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V29() ) set ) )) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ;

definition
let C be ( ( being_simple_closed_curve ) ( non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() ) Subset of ) ;
let n be ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ;
assume n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) is_sufficiently_large_for C : ( ( being_simple_closed_curve ) ( non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() ) Subset of ) ;
func Y-SpanStart (C,n) -> ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) means :: JORDAN11:def 3
( it : ( ( V26() V46(K7(C : ( ( ) ( ) RLTopStruct ) ,C : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,C : ( ( ) ( ) RLTopStruct ) ) ) ( V21() V24(K7(C : ( ( ) ( ) RLTopStruct ) ,C : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ) V25(C : ( ( ) ( ) RLTopStruct ) ) V26() V46(K7(C : ( ( ) ( ) RLTopStruct ) ,C : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,C : ( ( ) ( ) RLTopStruct ) ) ) Element of K6(K7(K7(C : ( ( ) ( ) RLTopStruct ) ,C : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,C : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) <= width (Gauge (C : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) Element of C : ( ( ) ( ) RLTopStruct ) ) )) : ( ( tabular ) ( V21() V24( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) V25(K292( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V153() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V29() ) set ) ) : ( ( ) ( ) M9( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V153() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V29() ) set ) )) ) V26() FinSequence-like tabular ) FinSequence of K292( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V153() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V29() ) set ) ) : ( ( ) ( ) M9( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V153() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V29() ) set ) )) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) & ( for k being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) st it : ( ( V26() V46(K7(C : ( ( ) ( ) RLTopStruct ) ,C : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,C : ( ( ) ( ) RLTopStruct ) ) ) ( V21() V24(K7(C : ( ( ) ( ) RLTopStruct ) ,C : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ) V25(C : ( ( ) ( ) RLTopStruct ) ) V26() V46(K7(C : ( ( ) ( ) RLTopStruct ) ,C : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,C : ( ( ) ( ) RLTopStruct ) ) ) Element of K6(K7(K7(C : ( ( ) ( ) RLTopStruct ) ,C : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,C : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) <= k : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) & k : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) <= ((2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) |^ (n : ( ( ) ( ) Element of C : ( ( ) ( ) RLTopStruct ) ) -' (ApproxIndex C : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) * ((Y-InitStart C : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) -' 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) + 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) holds
cell ((Gauge (C : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) Element of C : ( ( ) ( ) RLTopStruct ) ) )) : ( ( tabular ) ( V21() V24( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) V25(K292( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V153() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V29() ) set ) ) : ( ( ) ( ) M9( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V153() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V29() ) set ) )) ) V26() FinSequence-like tabular ) FinSequence of K292( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V153() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V29() ) set ) ) : ( ( ) ( ) M9( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V153() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V29() ) set ) )) ) ,((X-SpanStart (C : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) Element of C : ( ( ) ( ) RLTopStruct ) ) )) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) -' 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,k : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V153() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V29() ) set ) ) : ( ( ) ( non empty ) set ) ) c= BDD C : ( ( ) ( ) RLTopStruct ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V153() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V29() ) set ) ) : ( ( ) ( non empty ) set ) ) ) & ( for j being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) st j : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) <= width (Gauge (C : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) Element of C : ( ( ) ( ) RLTopStruct ) ) )) : ( ( tabular ) ( V21() V24( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) V25(K292( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V153() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V29() ) set ) ) : ( ( ) ( ) M9( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V153() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V29() ) set ) )) ) V26() FinSequence-like tabular ) FinSequence of K292( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V153() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V29() ) set ) ) : ( ( ) ( ) M9( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V153() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V29() ) set ) )) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) & ( for k being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) st j : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) <= k : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) & k : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) <= ((2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) |^ (n : ( ( ) ( ) Element of C : ( ( ) ( ) RLTopStruct ) ) -' (ApproxIndex C : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) * ((Y-InitStart C : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) -' 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) + 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) holds
cell ((Gauge (C : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) Element of C : ( ( ) ( ) RLTopStruct ) ) )) : ( ( tabular ) ( V21() V24( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) V25(K292( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V153() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V29() ) set ) ) : ( ( ) ( ) M9( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V153() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V29() ) set ) )) ) V26() FinSequence-like tabular ) FinSequence of K292( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V153() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V29() ) set ) ) : ( ( ) ( ) M9( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V153() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V29() ) set ) )) ) ,((X-SpanStart (C : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) Element of C : ( ( ) ( ) RLTopStruct ) ) )) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) -' 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,k : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V153() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V29() ) set ) ) : ( ( ) ( non empty ) set ) ) c= BDD C : ( ( ) ( ) RLTopStruct ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V153() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V29() ) set ) ) : ( ( ) ( non empty ) set ) ) ) holds
j : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) >= it : ( ( V26() V46(K7(C : ( ( ) ( ) RLTopStruct ) ,C : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,C : ( ( ) ( ) RLTopStruct ) ) ) ( V21() V24(K7(C : ( ( ) ( ) RLTopStruct ) ,C : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ) V25(C : ( ( ) ( ) RLTopStruct ) ) V26() V46(K7(C : ( ( ) ( ) RLTopStruct ) ,C : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,C : ( ( ) ( ) RLTopStruct ) ) ) Element of K6(K7(K7(C : ( ( ) ( ) RLTopStruct ) ,C : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,C : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) );
end;

theorem :: JORDAN11:4
for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) )
for C being ( ( being_simple_closed_curve ) ( non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() ) Subset of ) st n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) is_sufficiently_large_for C : ( ( being_simple_closed_curve ) ( non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() ) Subset of ) holds
X-SpanStart (C : ( ( being_simple_closed_curve ) ( non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() ) Subset of ) ,n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) = ((2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) |^ (n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) -' (ApproxIndex C : ( ( being_simple_closed_curve ) ( non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() ) Subset of ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) * ((X-SpanStart (C : ( ( being_simple_closed_curve ) ( non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() ) Subset of ) ,(ApproxIndex C : ( ( being_simple_closed_curve ) ( non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() ) Subset of ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) - 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V11() real integer ext-real ) Element of REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) ) : ( ( ) ( V11() real integer ext-real ) Element of REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) + 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V11() real integer ext-real ) Element of REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) ;

theorem :: JORDAN11:5
for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) )
for C being ( ( being_simple_closed_curve ) ( non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() ) Subset of ) st n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) is_sufficiently_large_for C : ( ( being_simple_closed_curve ) ( non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() ) Subset of ) holds
Y-SpanStart (C : ( ( being_simple_closed_curve ) ( non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() ) Subset of ) ,n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) <= ((2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) |^ (n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) -' (ApproxIndex C : ( ( being_simple_closed_curve ) ( non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() ) Subset of ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) * ((Y-InitStart C : ( ( being_simple_closed_curve ) ( non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() ) Subset of ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) -' 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) + 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: JORDAN11:6
for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) )
for C being ( ( being_simple_closed_curve ) ( non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() ) Subset of ) st n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) is_sufficiently_large_for C : ( ( being_simple_closed_curve ) ( non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() ) Subset of ) holds
cell ((Gauge (C : ( ( being_simple_closed_curve ) ( non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() ) Subset of ) ,n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( tabular ) ( V21() V23() V24( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) V25(K292( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V153() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V29() ) set ) ) : ( ( ) ( ) M9( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V153() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V29() ) set ) )) ) V26() FinSequence-like tabular V257() V258() V259() V260() ) FinSequence of K292( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V153() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V29() ) set ) ) : ( ( ) ( ) M9( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V153() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V29() ) set ) )) ) ,((X-SpanStart (C : ( ( being_simple_closed_curve ) ( non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() ) Subset of ) ,n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) -' 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,(Y-SpanStart (C : ( ( being_simple_closed_curve ) ( non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() ) Subset of ) ,n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V153() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V29() ) set ) ) : ( ( ) ( non empty ) set ) ) c= BDD C : ( ( being_simple_closed_curve ) ( non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() ) Subset of ) : ( ( ) ( non empty open ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V153() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V29() ) set ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: JORDAN11:7
for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) )
for C being ( ( being_simple_closed_curve ) ( non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() ) Subset of ) st n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) is_sufficiently_large_for C : ( ( being_simple_closed_curve ) ( non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() ) Subset of ) holds
( 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) < Y-SpanStart (C : ( ( being_simple_closed_curve ) ( non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() ) Subset of ) ,n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) & Y-SpanStart (C : ( ( being_simple_closed_curve ) ( non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() ) Subset of ) ,n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) <= width (Gauge (C : ( ( being_simple_closed_curve ) ( non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() ) Subset of ) ,n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( tabular ) ( V21() V23() V24( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) V25(K292( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V153() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V29() ) set ) ) : ( ( ) ( ) M9( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V153() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V29() ) set ) )) ) V26() FinSequence-like tabular V257() V258() V259() V260() ) FinSequence of K292( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V153() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V29() ) set ) ) : ( ( ) ( ) M9( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V153() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V29() ) set ) )) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) ;

theorem :: JORDAN11:8
for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) )
for C being ( ( being_simple_closed_curve ) ( non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() ) Subset of ) st n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) is_sufficiently_large_for C : ( ( being_simple_closed_curve ) ( non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() ) Subset of ) holds
[(X-SpanStart (C : ( ( being_simple_closed_curve ) ( non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() ) Subset of ) ,n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,(Y-SpanStart (C : ( ( being_simple_closed_curve ) ( non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() ) Subset of ) ,n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ] : ( ( ) ( ) set ) in Indices (Gauge (C : ( ( being_simple_closed_curve ) ( non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() ) Subset of ) ,n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( tabular ) ( V21() V23() V24( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) V25(K292( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V153() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V29() ) set ) ) : ( ( ) ( ) M9( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V153() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V29() ) set ) )) ) V26() FinSequence-like tabular V257() V258() V259() V260() ) FinSequence of K292( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V153() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V29() ) set ) ) : ( ( ) ( ) M9( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V153() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V29() ) set ) )) ) : ( ( ) ( ) set ) ;

theorem :: JORDAN11:9
for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) )
for C being ( ( being_simple_closed_curve ) ( non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() ) Subset of ) st n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) is_sufficiently_large_for C : ( ( being_simple_closed_curve ) ( non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() ) Subset of ) holds
[((X-SpanStart (C : ( ( being_simple_closed_curve ) ( non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() ) Subset of ) ,n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) -' 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,(Y-SpanStart (C : ( ( being_simple_closed_curve ) ( non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() ) Subset of ) ,n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ] : ( ( ) ( ) set ) in Indices (Gauge (C : ( ( being_simple_closed_curve ) ( non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() ) Subset of ) ,n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( tabular ) ( V21() V23() V24( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) V25(K292( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V153() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V29() ) set ) ) : ( ( ) ( ) M9( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V153() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V29() ) set ) )) ) V26() FinSequence-like tabular V257() V258() V259() V260() ) FinSequence of K292( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V153() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V29() ) set ) ) : ( ( ) ( ) M9( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V153() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V29() ) set ) )) ) : ( ( ) ( ) set ) ;

theorem :: JORDAN11:10
for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) )
for C being ( ( being_simple_closed_curve ) ( non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() ) Subset of ) st n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) is_sufficiently_large_for C : ( ( being_simple_closed_curve ) ( non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() ) Subset of ) holds
cell ((Gauge (C : ( ( being_simple_closed_curve ) ( non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() ) Subset of ) ,n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( tabular ) ( V21() V23() V24( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) V25(K292( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V153() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V29() ) set ) ) : ( ( ) ( ) M9( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V153() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V29() ) set ) )) ) V26() FinSequence-like tabular V257() V258() V259() V260() ) FinSequence of K292( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V153() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V29() ) set ) ) : ( ( ) ( ) M9( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V153() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V29() ) set ) )) ) ,((X-SpanStart (C : ( ( being_simple_closed_curve ) ( non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() ) Subset of ) ,n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) -' 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,((Y-SpanStart (C : ( ( being_simple_closed_curve ) ( non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() ) Subset of ) ,n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) -' 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V153() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V29() ) set ) ) : ( ( ) ( non empty ) set ) ) meets C : ( ( being_simple_closed_curve ) ( non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() ) Subset of ) ;

theorem :: JORDAN11:11
for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) )
for C being ( ( being_simple_closed_curve ) ( non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() ) Subset of ) st n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) is_sufficiently_large_for C : ( ( being_simple_closed_curve ) ( non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() ) Subset of ) holds
cell ((Gauge (C : ( ( being_simple_closed_curve ) ( non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() ) Subset of ) ,n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( tabular ) ( V21() V23() V24( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) V25(K292( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V153() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V29() ) set ) ) : ( ( ) ( ) M9( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V153() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V29() ) set ) )) ) V26() FinSequence-like tabular V257() V258() V259() V260() ) FinSequence of K292( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V153() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V29() ) set ) ) : ( ( ) ( ) M9( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V153() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V29() ) set ) )) ) ,((X-SpanStart (C : ( ( being_simple_closed_curve ) ( non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() ) Subset of ) ,n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) -' 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,(Y-SpanStart (C : ( ( being_simple_closed_curve ) ( non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() ) Subset of ) ,n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V153() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V29() ) set ) ) : ( ( ) ( non empty ) set ) ) misses C : ( ( being_simple_closed_curve ) ( non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() ) Subset of ) ;

begin

theorem :: JORDAN11:12
for C being ( ( being_simple_closed_curve ) ( non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() ) Subset of )
for D being ( ( being_simple_closed_curve ) ( non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() ) Simple_closed_curve) holds UBD C : ( ( being_simple_closed_curve ) ( non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() ) Subset of ) : ( ( ) ( non empty open connected ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V153() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V29() ) set ) ) : ( ( ) ( non empty ) set ) ) meets UBD D : ( ( being_simple_closed_curve ) ( non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() ) Simple_closed_curve) : ( ( ) ( non empty open connected ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V153() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V29() ) set ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: JORDAN11:13
for C being ( ( being_simple_closed_curve ) ( non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() ) Subset of )
for q, p being ( ( ) ( V41(2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) FinSequence-like V122() ) Point of ( ( ) ( non empty V29() ) set ) ) st q : ( ( ) ( V41(2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) FinSequence-like V122() ) Point of ( ( ) ( non empty V29() ) set ) ) in UBD C : ( ( being_simple_closed_curve ) ( non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() ) Subset of ) : ( ( ) ( non empty open connected ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V153() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V29() ) set ) ) : ( ( ) ( non empty ) set ) ) & p : ( ( ) ( V41(2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) FinSequence-like V122() ) Point of ( ( ) ( non empty V29() ) set ) ) in BDD C : ( ( being_simple_closed_curve ) ( non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() ) Subset of ) : ( ( ) ( non empty open ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V153() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V29() ) set ) ) : ( ( ) ( non empty ) set ) ) holds
dist (q : ( ( ) ( V41(2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) FinSequence-like V122() ) Point of ( ( ) ( non empty V29() ) set ) ) ,C : ( ( being_simple_closed_curve ) ( non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() ) Subset of ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) < dist (q : ( ( ) ( V41(2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) FinSequence-like V122() ) Point of ( ( ) ( non empty V29() ) set ) ) ,p : ( ( ) ( V41(2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) FinSequence-like V122() ) Point of ( ( ) ( non empty V29() ) set ) ) ) : ( ( ) ( V11() real ext-real non negative ) Element of REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) ;

theorem :: JORDAN11:14
for C being ( ( being_simple_closed_curve ) ( non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() ) Subset of )
for p being ( ( ) ( V41(2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) FinSequence-like V122() ) Point of ( ( ) ( non empty V29() ) set ) ) st not p : ( ( ) ( V41(2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) FinSequence-like V122() ) Point of ( ( ) ( non empty V29() ) set ) ) in BDD C : ( ( being_simple_closed_curve ) ( non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() ) Subset of ) : ( ( ) ( non empty open ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V153() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V29() ) set ) ) : ( ( ) ( non empty ) set ) ) holds
dist (p : ( ( ) ( V41(2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) FinSequence-like V122() ) Point of ( ( ) ( non empty V29() ) set ) ) ,C : ( ( being_simple_closed_curve ) ( non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() ) Subset of ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) <= dist (p : ( ( ) ( V41(2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) FinSequence-like V122() ) Point of ( ( ) ( non empty V29() ) set ) ) ,(BDD C : ( ( being_simple_closed_curve ) ( non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() ) Subset of ) ) : ( ( ) ( non empty open ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V153() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V29() ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) ;

theorem :: JORDAN11:15
for C being ( ( being_simple_closed_curve ) ( non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() ) Subset of )
for D being ( ( being_simple_closed_curve ) ( non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() ) Simple_closed_curve) holds
( not C : ( ( being_simple_closed_curve ) ( non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() ) Subset of ) c= BDD D : ( ( being_simple_closed_curve ) ( non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() ) Simple_closed_curve) : ( ( ) ( non empty open ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V153() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V29() ) set ) ) : ( ( ) ( non empty ) set ) ) or not D : ( ( being_simple_closed_curve ) ( non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() ) Simple_closed_curve) c= BDD C : ( ( being_simple_closed_curve ) ( non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() ) Subset of ) : ( ( ) ( non empty open ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V153() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V29() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: JORDAN11:16
for C being ( ( being_simple_closed_curve ) ( non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() ) Subset of )
for D being ( ( being_simple_closed_curve ) ( non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() ) Simple_closed_curve) st C : ( ( being_simple_closed_curve ) ( non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() ) Subset of ) c= BDD D : ( ( being_simple_closed_curve ) ( non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() ) Simple_closed_curve) : ( ( ) ( non empty open ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V153() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V29() ) set ) ) : ( ( ) ( non empty ) set ) ) holds
D : ( ( being_simple_closed_curve ) ( non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() ) Simple_closed_curve) c= UBD C : ( ( being_simple_closed_curve ) ( non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() ) Subset of ) : ( ( ) ( non empty open connected ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V153() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V29() ) set ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: JORDAN11:17
for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) )
for C being ( ( being_simple_closed_curve ) ( non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() ) Subset of ) holds L~ (Cage (C : ( ( being_simple_closed_curve ) ( non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() ) Subset of ) ,n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V49() V130() V131() V132() V133() V134() V135() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( non empty V28() V199( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V153() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V29() ) set ) ) special unfolded s.c.c. standard V236() ) ( non empty V21() V24( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) V25( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V153() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V29() ) set ) ) V26() V28() FinSequence-like V199( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V153() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V29() ) set ) ) special unfolded s.c.c. standard V236() ) FinSequence of the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V153() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V29() ) set ) ) : ( ( ) ( non empty proper closed V91( TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V153() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous ) RLTopStruct ) ) connected bounded being_simple_closed_curve compact V233() V234() ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V153() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V29() ) set ) ) : ( ( ) ( non empty ) set ) ) c= UBD C : ( ( being_simple_closed_curve ) ( non empty proper closed connected bounded being_simple_closed_curve compact V233() V234() ) Subset of ) : ( ( ) ( non empty open connected ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative V49() V130() V131() V132() V133() V134() V135() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V130() V131() V132() V133() V134() V135() V136() left_end bounded_below ) Element of K6(REAL : ( ( ) ( non empty V34() V130() V131() V132() V136() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V153() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V29() ) set ) ) : ( ( ) ( non empty ) set ) ) ;