:: JORDAN21 semantic presentation

begin

theorem :: JORDAN21:1
for n being ( ( ) ( natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) )
for p being ( ( ) ( V43(b1 : ( ( ) ( natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Point of ( ( ) ( non empty V30() ) set ) ) holds {p : ( ( ) ( V43(b1 : ( ( ) ( natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Point of ( ( ) ( non empty V30() ) set ) ) } : ( ( ) ( non empty ) Element of K6( the carrier of (TOP-REAL b1 : ( ( ) ( natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) : ( ( ) ( ) set ) ) is bounded ;

theorem :: JORDAN21:2
for s1, t being ( ( real ) ( V11() real ext-real ) number )
for P being ( ( ) ( ) Subset of ) st P : ( ( ) ( ) Subset of ) = { |[s : ( ( ) ( V11() real ext-real ) Real) ,t : ( ( real ) ( V11() real ext-real ) number ) ]| : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) where s is ( ( ) ( V11() real ext-real ) Real) : s1 : ( ( real ) ( V11() real ext-real ) number ) < s : ( ( ) ( V11() real ext-real ) Real) } holds
P : ( ( ) ( ) Subset of ) is convex ;

theorem :: JORDAN21:3
for s2, t being ( ( real ) ( V11() real ext-real ) number )
for P being ( ( ) ( ) Subset of ) st P : ( ( ) ( ) Subset of ) = { |[s : ( ( ) ( V11() real ext-real ) Real) ,t : ( ( real ) ( V11() real ext-real ) number ) ]| : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) where s is ( ( ) ( V11() real ext-real ) Real) : s : ( ( ) ( V11() real ext-real ) Real) < s2 : ( ( real ) ( V11() real ext-real ) number ) } holds
P : ( ( ) ( ) Subset of ) is convex ;

theorem :: JORDAN21:4
for s, t1 being ( ( real ) ( V11() real ext-real ) number )
for P being ( ( ) ( ) Subset of ) st P : ( ( ) ( ) Subset of ) = { |[s : ( ( real ) ( V11() real ext-real ) number ) ,t : ( ( ) ( V11() real ext-real ) Real) ]| : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) where t is ( ( ) ( V11() real ext-real ) Real) : t1 : ( ( real ) ( V11() real ext-real ) number ) < t : ( ( ) ( V11() real ext-real ) Real) } holds
P : ( ( ) ( ) Subset of ) is convex ;

theorem :: JORDAN21:5
for s, t2 being ( ( real ) ( V11() real ext-real ) number )
for P being ( ( ) ( ) Subset of ) st P : ( ( ) ( ) Subset of ) = { |[s : ( ( real ) ( V11() real ext-real ) number ) ,t : ( ( ) ( V11() real ext-real ) Real) ]| : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) where t is ( ( ) ( V11() real ext-real ) Real) : t : ( ( ) ( V11() real ext-real ) Real) < t2 : ( ( real ) ( V11() real ext-real ) number ) } holds
P : ( ( ) ( ) Subset of ) is convex ;

theorem :: JORDAN21:6
for p being ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Point of ( ( ) ( non empty V30() ) set ) ) holds (north_halfline p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Point of ( ( ) ( non empty V30() ) set ) ) ) : ( ( ) ( non empty ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) : ( ( ) ( ) set ) ) \ {p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Point of ( ( ) ( non empty V30() ) set ) ) } : ( ( ) ( non empty ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) : ( ( ) ( ) set ) ) is convex ;

theorem :: JORDAN21:7
for p being ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Point of ( ( ) ( non empty V30() ) set ) ) holds (south_halfline p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Point of ( ( ) ( non empty V30() ) set ) ) ) : ( ( ) ( non empty ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) : ( ( ) ( ) set ) ) \ {p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Point of ( ( ) ( non empty V30() ) set ) ) } : ( ( ) ( non empty ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) : ( ( ) ( ) set ) ) is convex ;

theorem :: JORDAN21:8
for p being ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Point of ( ( ) ( non empty V30() ) set ) ) holds (west_halfline p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Point of ( ( ) ( non empty V30() ) set ) ) ) : ( ( ) ( non empty ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) : ( ( ) ( ) set ) ) \ {p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Point of ( ( ) ( non empty V30() ) set ) ) } : ( ( ) ( non empty ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) : ( ( ) ( ) set ) ) is convex ;

theorem :: JORDAN21:9
for p being ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Point of ( ( ) ( non empty V30() ) set ) ) holds (east_halfline p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Point of ( ( ) ( non empty V30() ) set ) ) ) : ( ( ) ( non empty ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) : ( ( ) ( ) set ) ) \ {p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Point of ( ( ) ( non empty V30() ) set ) ) } : ( ( ) ( non empty ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) : ( ( ) ( ) set ) ) is convex ;

theorem :: JORDAN21:10
for A being ( ( ) ( ) Subset of ( ( ) ( ) set ) ) holds UBD A : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) : ( ( ) ( ) set ) ) misses A : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) ;

theorem :: JORDAN21:11
for P being ( ( ) ( ) Subset of ( ( ) ( ) set ) )
for p1, p2, q1, q2 being ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Point of ( ( ) ( non empty V30() ) set ) ) st P : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) is_an_arc_of p1 : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Point of ( ( ) ( non empty V30() ) set ) ) ,p2 : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Point of ( ( ) ( non empty V30() ) set ) ) & p1 : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Point of ( ( ) ( non empty V30() ) set ) ) <> q1 : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Point of ( ( ) ( non empty V30() ) set ) ) & p2 : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Point of ( ( ) ( non empty V30() ) set ) ) <> q2 : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Point of ( ( ) ( non empty V30() ) set ) ) holds
( not p1 : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Point of ( ( ) ( non empty V30() ) set ) ) in Segment (P : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) ,p1 : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Point of ( ( ) ( non empty V30() ) set ) ) ,p2 : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Point of ( ( ) ( non empty V30() ) set ) ) ,q1 : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Point of ( ( ) ( non empty V30() ) set ) ) ,q2 : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Point of ( ( ) ( non empty V30() ) set ) ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) : ( ( ) ( ) set ) ) & not p2 : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Point of ( ( ) ( non empty V30() ) set ) ) in Segment (P : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) ,p1 : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Point of ( ( ) ( non empty V30() ) set ) ) ,p2 : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Point of ( ( ) ( non empty V30() ) set ) ) ,q1 : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Point of ( ( ) ( non empty V30() ) set ) ) ,q2 : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Point of ( ( ) ( non empty V30() ) set ) ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) : ( ( ) ( ) set ) ) ) ;

definition
let D be ( ( ) ( ) Subset of ) ;
attr D is with_the_max_arc means :: JORDAN21:def 1
D : ( ( ) ( ) RLTopStruct ) meets Vertical_Line (((W-bound D : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) + (E-bound D : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) / 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) : ( ( ) ( ) set ) ) ;
end;

registration
cluster with_the_max_arc -> non empty for ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) : ( ( ) ( ) set ) ) ;
end;

registration
cluster being_simple_closed_curve -> being_simple_closed_curve with_the_max_arc for ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) : ( ( ) ( ) set ) ) ;
end;

registration
cluster non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve with_the_max_arc for ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) : ( ( ) ( ) set ) ) ;
end;

theorem :: JORDAN21:12
for D being ( ( with_the_max_arc ) ( non empty with_the_max_arc ) Subset of ) holds not proj2 : ( ( V27() V33( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) , REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ) ( V22() V25( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) V26( REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) V27() V33( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) , REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) V138() V139() V140() ) Element of K6(K7( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ,REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( V138() V139() V140() ) set ) ) : ( ( ) ( ) set ) ) .: (D : ( ( with_the_max_arc ) ( non empty with_the_max_arc ) Subset of ) /\ (Vertical_Line (((W-bound D : ( ( with_the_max_arc ) ( non empty with_the_max_arc ) Subset of ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) + (E-bound D : ( ( with_the_max_arc ) ( non empty with_the_max_arc ) Subset of ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) / 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V148() V149() V150() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) is empty ;

theorem :: JORDAN21:13
for C being ( ( compact ) ( closed compact bounded ) Subset of ) holds
( proj2 : ( ( V27() V33( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) , REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ) ( V22() V25( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) V26( REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) V27() V33( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) , REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) V138() V139() V140() ) Element of K6(K7( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ,REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( V138() V139() V140() ) set ) ) : ( ( ) ( ) set ) ) .: (C : ( ( compact ) ( closed compact bounded ) Subset of ) /\ (Vertical_Line (((W-bound C : ( ( compact ) ( closed compact bounded ) Subset of ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) + (E-bound C : ( ( compact ) ( closed compact bounded ) Subset of ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) / 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V148() V149() V150() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) is closed & proj2 : ( ( V27() V33( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) , REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ) ( V22() V25( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) V26( REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) V27() V33( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) , REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) V138() V139() V140() ) Element of K6(K7( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ,REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( V138() V139() V140() ) set ) ) : ( ( ) ( ) set ) ) .: (C : ( ( compact ) ( closed compact bounded ) Subset of ) /\ (Vertical_Line (((W-bound C : ( ( compact ) ( closed compact bounded ) Subset of ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) + (E-bound C : ( ( compact ) ( closed compact bounded ) Subset of ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) / 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V148() V149() V150() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) is bounded_below & proj2 : ( ( V27() V33( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) , REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ) ( V22() V25( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) V26( REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) V27() V33( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) , REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) V138() V139() V140() ) Element of K6(K7( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ,REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( V138() V139() V140() ) set ) ) : ( ( ) ( ) set ) ) .: (C : ( ( compact ) ( closed compact bounded ) Subset of ) /\ (Vertical_Line (((W-bound C : ( ( compact ) ( closed compact bounded ) Subset of ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) + (E-bound C : ( ( compact ) ( closed compact bounded ) Subset of ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) / 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V148() V149() V150() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) is bounded_above ) ;

begin

theorem :: JORDAN21:14
for C being ( ( being_simple_closed_curve ) ( non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve ) Simple_closed_curve) holds Lower_Middle_Point C : ( ( being_simple_closed_curve ) ( non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve with_the_max_arc ) Simple_closed_curve) : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) in C : ( ( being_simple_closed_curve ) ( non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve with_the_max_arc ) Simple_closed_curve) ;

theorem :: JORDAN21:15
for C being ( ( being_simple_closed_curve ) ( non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve ) Simple_closed_curve) holds (Lower_Middle_Point C : ( ( being_simple_closed_curve ) ( non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve with_the_max_arc ) Simple_closed_curve) ) : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) <> (Upper_Middle_Point C : ( ( being_simple_closed_curve ) ( non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve with_the_max_arc ) Simple_closed_curve) ) : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ;

theorem :: JORDAN21:16
for C being ( ( being_simple_closed_curve ) ( non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve ) Simple_closed_curve) holds Lower_Middle_Point C : ( ( being_simple_closed_curve ) ( non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve with_the_max_arc ) Simple_closed_curve) : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) <> Upper_Middle_Point C : ( ( being_simple_closed_curve ) ( non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve with_the_max_arc ) Simple_closed_curve) : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) ;

begin

theorem :: JORDAN21:17
for C being ( ( being_simple_closed_curve ) ( non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve ) Simple_closed_curve) holds W-bound C : ( ( being_simple_closed_curve ) ( non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve with_the_max_arc ) Simple_closed_curve) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) = W-bound (Upper_Arc C : ( ( being_simple_closed_curve ) ( non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve with_the_max_arc ) Simple_closed_curve) ) : ( ( non empty ) ( non empty closed compact bounded ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ;

theorem :: JORDAN21:18
for C being ( ( being_simple_closed_curve ) ( non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve ) Simple_closed_curve) holds E-bound C : ( ( being_simple_closed_curve ) ( non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve with_the_max_arc ) Simple_closed_curve) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) = E-bound (Upper_Arc C : ( ( being_simple_closed_curve ) ( non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve with_the_max_arc ) Simple_closed_curve) ) : ( ( non empty ) ( non empty closed compact bounded ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ;

theorem :: JORDAN21:19
for C being ( ( being_simple_closed_curve ) ( non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve ) Simple_closed_curve) holds W-bound C : ( ( being_simple_closed_curve ) ( non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve with_the_max_arc ) Simple_closed_curve) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) = W-bound (Lower_Arc C : ( ( being_simple_closed_curve ) ( non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve with_the_max_arc ) Simple_closed_curve) ) : ( ( non empty ) ( non empty closed compact bounded ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ;

theorem :: JORDAN21:20
for C being ( ( being_simple_closed_curve ) ( non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve ) Simple_closed_curve) holds E-bound C : ( ( being_simple_closed_curve ) ( non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve with_the_max_arc ) Simple_closed_curve) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) = E-bound (Lower_Arc C : ( ( being_simple_closed_curve ) ( non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve with_the_max_arc ) Simple_closed_curve) ) : ( ( non empty ) ( non empty closed compact bounded ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ;

theorem :: JORDAN21:21
for C being ( ( being_simple_closed_curve ) ( non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve ) Simple_closed_curve) holds
( not (Upper_Arc C : ( ( being_simple_closed_curve ) ( non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve with_the_max_arc ) Simple_closed_curve) ) : ( ( non empty ) ( non empty closed compact bounded ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) : ( ( ) ( ) set ) ) /\ (Vertical_Line (((W-bound C : ( ( being_simple_closed_curve ) ( non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve with_the_max_arc ) Simple_closed_curve) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) + (E-bound C : ( ( being_simple_closed_curve ) ( non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve with_the_max_arc ) Simple_closed_curve) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) / 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) : ( ( ) ( ) set ) ) is empty & not proj2 : ( ( V27() V33( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) , REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ) ( V22() V25( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) V26( REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) V27() V33( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) , REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) V138() V139() V140() ) Element of K6(K7( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ,REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( V138() V139() V140() ) set ) ) : ( ( ) ( ) set ) ) .: ((Upper_Arc C : ( ( being_simple_closed_curve ) ( non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve with_the_max_arc ) Simple_closed_curve) ) : ( ( non empty ) ( non empty closed compact bounded ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) : ( ( ) ( ) set ) ) /\ (Vertical_Line (((W-bound C : ( ( being_simple_closed_curve ) ( non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve with_the_max_arc ) Simple_closed_curve) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) + (E-bound C : ( ( being_simple_closed_curve ) ( non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve with_the_max_arc ) Simple_closed_curve) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) / 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V148() V149() V150() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) is empty ) ;

theorem :: JORDAN21:22
for C being ( ( being_simple_closed_curve ) ( non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve ) Simple_closed_curve) holds
( not (Lower_Arc C : ( ( being_simple_closed_curve ) ( non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve with_the_max_arc ) Simple_closed_curve) ) : ( ( non empty ) ( non empty closed compact bounded ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) : ( ( ) ( ) set ) ) /\ (Vertical_Line (((W-bound C : ( ( being_simple_closed_curve ) ( non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve with_the_max_arc ) Simple_closed_curve) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) + (E-bound C : ( ( being_simple_closed_curve ) ( non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve with_the_max_arc ) Simple_closed_curve) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) / 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) : ( ( ) ( ) set ) ) is empty & not proj2 : ( ( V27() V33( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) , REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ) ( V22() V25( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) V26( REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) V27() V33( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) , REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) V138() V139() V140() ) Element of K6(K7( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ,REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( V138() V139() V140() ) set ) ) : ( ( ) ( ) set ) ) .: ((Lower_Arc C : ( ( being_simple_closed_curve ) ( non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve with_the_max_arc ) Simple_closed_curve) ) : ( ( non empty ) ( non empty closed compact bounded ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) : ( ( ) ( ) set ) ) /\ (Vertical_Line (((W-bound C : ( ( being_simple_closed_curve ) ( non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve with_the_max_arc ) Simple_closed_curve) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) + (E-bound C : ( ( being_simple_closed_curve ) ( non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve with_the_max_arc ) Simple_closed_curve) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) / 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V148() V149() V150() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) is empty ) ;

theorem :: JORDAN21:23
for C being ( ( being_simple_closed_curve ) ( non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve ) Simple_closed_curve)
for P being ( ( connected compact ) ( closed connected compact bounded ) Subset of ) st P : ( ( connected compact ) ( closed connected compact bounded ) Subset of ) c= C : ( ( being_simple_closed_curve ) ( non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve with_the_max_arc ) Simple_closed_curve) & W-min C : ( ( being_simple_closed_curve ) ( non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve with_the_max_arc ) Simple_closed_curve) : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) in P : ( ( connected compact ) ( closed connected compact bounded ) Subset of ) & E-max C : ( ( being_simple_closed_curve ) ( non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve with_the_max_arc ) Simple_closed_curve) : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) in P : ( ( connected compact ) ( closed connected compact bounded ) Subset of ) & not Upper_Arc C : ( ( being_simple_closed_curve ) ( non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve with_the_max_arc ) Simple_closed_curve) : ( ( non empty ) ( non empty closed compact bounded ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) : ( ( ) ( ) set ) ) c= P : ( ( connected compact ) ( closed connected compact bounded ) Subset of ) holds
Lower_Arc C : ( ( being_simple_closed_curve ) ( non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve with_the_max_arc ) Simple_closed_curve) : ( ( non empty ) ( non empty closed compact bounded ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) : ( ( ) ( ) set ) ) c= P : ( ( connected compact ) ( closed connected compact bounded ) Subset of ) ;

registration
let C be ( ( being_simple_closed_curve ) ( non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve ) Simple_closed_curve) ;
cluster Lower_Arc C : ( ( being_simple_closed_curve ) ( non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve with_the_max_arc ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) : ( ( ) ( ) set ) ) : ( ( non empty ) ( non empty closed compact bounded ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) : ( ( ) ( ) set ) ) -> non empty with_the_max_arc ;
cluster Upper_Arc C : ( ( being_simple_closed_curve ) ( non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve with_the_max_arc ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) : ( ( ) ( ) set ) ) : ( ( non empty ) ( non empty closed compact bounded ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) : ( ( ) ( ) set ) ) -> non empty with_the_max_arc ;
end;

begin

definition
let P be ( ( ) ( ) Subset of ( ( ) ( ) set ) ) ;
func UMP P -> ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Point of ( ( ) ( non empty V30() ) set ) ) equals :: JORDAN21:def 2
|[(((E-bound P : ( ( non empty ) ( non empty ) L7()) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) + (W-bound P : ( ( non empty ) ( non empty ) L7()) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) / 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ,(upper_bound (proj2 : ( ( V27() V33( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) , REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ) ( V22() V25( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) V26( REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) V27() V33( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) , REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) V138() V139() V140() ) Element of K6(K7( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ,REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( V138() V139() V140() ) set ) ) : ( ( ) ( ) set ) ) .: (P : ( ( non empty ) ( non empty ) L7()) /\ (Vertical_Line (((E-bound P : ( ( non empty ) ( non empty ) L7()) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) + (W-bound P : ( ( non empty ) ( non empty ) L7()) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) / 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V148() V149() V150() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ]| : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) ;
func LMP P -> ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Point of ( ( ) ( non empty V30() ) set ) ) equals :: JORDAN21:def 3
|[(((E-bound P : ( ( non empty ) ( non empty ) L7()) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) + (W-bound P : ( ( non empty ) ( non empty ) L7()) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) / 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ,(lower_bound (proj2 : ( ( V27() V33( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) , REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ) ( V22() V25( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) V26( REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) V27() V33( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) , REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) V138() V139() V140() ) Element of K6(K7( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ,REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( V138() V139() V140() ) set ) ) : ( ( ) ( ) set ) ) .: (P : ( ( non empty ) ( non empty ) L7()) /\ (Vertical_Line (((E-bound P : ( ( non empty ) ( non empty ) L7()) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) + (W-bound P : ( ( non empty ) ( non empty ) L7()) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) / 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V148() V149() V150() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ]| : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) ;
end;

theorem :: JORDAN21:24
for C being ( ( compact non vertical ) ( non empty closed compact bounded non vertical ) Subset of ) holds UMP C : ( ( compact non vertical ) ( non empty closed compact bounded non vertical ) Subset of ) : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Point of ( ( ) ( non empty V30() ) set ) ) <> W-min C : ( ( compact non vertical ) ( non empty closed compact bounded non vertical ) Subset of ) : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) ;

theorem :: JORDAN21:25
for C being ( ( compact non vertical ) ( non empty closed compact bounded non vertical ) Subset of ) holds UMP C : ( ( compact non vertical ) ( non empty closed compact bounded non vertical ) Subset of ) : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Point of ( ( ) ( non empty V30() ) set ) ) <> E-max C : ( ( compact non vertical ) ( non empty closed compact bounded non vertical ) Subset of ) : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) ;

theorem :: JORDAN21:26
for C being ( ( compact non vertical ) ( non empty closed compact bounded non vertical ) Subset of ) holds LMP C : ( ( compact non vertical ) ( non empty closed compact bounded non vertical ) Subset of ) : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Point of ( ( ) ( non empty V30() ) set ) ) <> W-min C : ( ( compact non vertical ) ( non empty closed compact bounded non vertical ) Subset of ) : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) ;

theorem :: JORDAN21:27
for C being ( ( compact non vertical ) ( non empty closed compact bounded non vertical ) Subset of ) holds LMP C : ( ( compact non vertical ) ( non empty closed compact bounded non vertical ) Subset of ) : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Point of ( ( ) ( non empty V30() ) set ) ) <> E-max C : ( ( compact non vertical ) ( non empty closed compact bounded non vertical ) Subset of ) : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) ;

theorem :: JORDAN21:28
for p being ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Point of ( ( ) ( non empty V30() ) set ) )
for C being ( ( compact ) ( closed compact bounded ) Subset of ) st p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Point of ( ( ) ( non empty V30() ) set ) ) in C : ( ( compact ) ( closed compact bounded ) Subset of ) /\ (Vertical_Line (((W-bound C : ( ( compact ) ( closed compact bounded ) Subset of ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) + (E-bound C : ( ( compact ) ( closed compact bounded ) Subset of ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) / 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) : ( ( ) ( ) set ) ) holds
p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Point of ( ( ) ( non empty V30() ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) <= (UMP C : ( ( compact ) ( closed compact bounded ) Subset of ) ) : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Point of ( ( ) ( non empty V30() ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ;

theorem :: JORDAN21:29
for p being ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Point of ( ( ) ( non empty V30() ) set ) )
for C being ( ( compact ) ( closed compact bounded ) Subset of ) st p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Point of ( ( ) ( non empty V30() ) set ) ) in C : ( ( compact ) ( closed compact bounded ) Subset of ) /\ (Vertical_Line (((W-bound C : ( ( compact ) ( closed compact bounded ) Subset of ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) + (E-bound C : ( ( compact ) ( closed compact bounded ) Subset of ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) / 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) : ( ( ) ( ) set ) ) holds
(LMP C : ( ( compact ) ( closed compact bounded ) Subset of ) ) : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Point of ( ( ) ( non empty V30() ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) <= p : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Point of ( ( ) ( non empty V30() ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ;

theorem :: JORDAN21:30
for D being ( ( compact with_the_max_arc ) ( non empty closed compact bounded with_the_max_arc ) Subset of ) holds UMP D : ( ( compact with_the_max_arc ) ( non empty closed compact bounded with_the_max_arc ) Subset of ) : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Point of ( ( ) ( non empty V30() ) set ) ) in D : ( ( compact with_the_max_arc ) ( non empty closed compact bounded with_the_max_arc ) Subset of ) ;

theorem :: JORDAN21:31
for D being ( ( compact with_the_max_arc ) ( non empty closed compact bounded with_the_max_arc ) Subset of ) holds LMP D : ( ( compact with_the_max_arc ) ( non empty closed compact bounded with_the_max_arc ) Subset of ) : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Point of ( ( ) ( non empty V30() ) set ) ) in D : ( ( compact with_the_max_arc ) ( non empty closed compact bounded with_the_max_arc ) Subset of ) ;

theorem :: JORDAN21:32
for P being ( ( ) ( ) Subset of ) holds LSeg ((UMP P : ( ( ) ( ) Subset of ) ) : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Point of ( ( ) ( non empty V30() ) set ) ) ,|[(((W-bound P : ( ( ) ( ) Subset of ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) + (E-bound P : ( ( ) ( ) Subset of ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) / 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ,(N-bound P : ( ( ) ( ) Subset of ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ]| : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) ) : ( ( ) ( non empty connected convex ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) : ( ( ) ( ) set ) ) is vertical ;

theorem :: JORDAN21:33
for P being ( ( ) ( ) Subset of ) holds LSeg ((LMP P : ( ( ) ( ) Subset of ) ) : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Point of ( ( ) ( non empty V30() ) set ) ) ,|[(((W-bound P : ( ( ) ( ) Subset of ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) + (E-bound P : ( ( ) ( ) Subset of ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) / 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ,(S-bound P : ( ( ) ( ) Subset of ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ]| : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) ) : ( ( ) ( non empty connected convex ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) : ( ( ) ( ) set ) ) is vertical ;

theorem :: JORDAN21:34
for D being ( ( compact with_the_max_arc ) ( non empty closed compact bounded with_the_max_arc ) Subset of ) holds (LSeg ((UMP D : ( ( compact with_the_max_arc ) ( non empty closed compact bounded with_the_max_arc ) Subset of ) ) : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Point of ( ( ) ( non empty V30() ) set ) ) ,|[(((W-bound D : ( ( compact with_the_max_arc ) ( non empty closed compact bounded with_the_max_arc ) Subset of ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) + (E-bound D : ( ( compact with_the_max_arc ) ( non empty closed compact bounded with_the_max_arc ) Subset of ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) / 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ,(N-bound D : ( ( compact with_the_max_arc ) ( non empty closed compact bounded with_the_max_arc ) Subset of ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ]| : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) )) : ( ( ) ( non empty connected convex ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) : ( ( ) ( ) set ) ) /\ D : ( ( compact with_the_max_arc ) ( non empty closed compact bounded with_the_max_arc ) Subset of ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) : ( ( ) ( ) set ) ) = {(UMP D : ( ( compact with_the_max_arc ) ( non empty closed compact bounded with_the_max_arc ) Subset of ) ) : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Point of ( ( ) ( non empty V30() ) set ) ) } : ( ( ) ( non empty ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: JORDAN21:35
for D being ( ( compact with_the_max_arc ) ( non empty closed compact bounded with_the_max_arc ) Subset of ) holds (LSeg ((LMP D : ( ( compact with_the_max_arc ) ( non empty closed compact bounded with_the_max_arc ) Subset of ) ) : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Point of ( ( ) ( non empty V30() ) set ) ) ,|[(((W-bound D : ( ( compact with_the_max_arc ) ( non empty closed compact bounded with_the_max_arc ) Subset of ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) + (E-bound D : ( ( compact with_the_max_arc ) ( non empty closed compact bounded with_the_max_arc ) Subset of ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) / 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ,(S-bound D : ( ( compact with_the_max_arc ) ( non empty closed compact bounded with_the_max_arc ) Subset of ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ]| : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) )) : ( ( ) ( non empty connected convex ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) : ( ( ) ( ) set ) ) /\ D : ( ( compact with_the_max_arc ) ( non empty closed compact bounded with_the_max_arc ) Subset of ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) : ( ( ) ( ) set ) ) = {(LMP D : ( ( compact with_the_max_arc ) ( non empty closed compact bounded with_the_max_arc ) Subset of ) ) : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Point of ( ( ) ( non empty V30() ) set ) ) } : ( ( ) ( non empty ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: JORDAN21:36
for C being ( ( being_simple_closed_curve ) ( non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve ) Simple_closed_curve) holds (LMP C : ( ( being_simple_closed_curve ) ( non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve with_the_max_arc ) Simple_closed_curve) ) : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Point of ( ( ) ( non empty V30() ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) < (UMP C : ( ( being_simple_closed_curve ) ( non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve with_the_max_arc ) Simple_closed_curve) ) : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Point of ( ( ) ( non empty V30() ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ;

theorem :: JORDAN21:37
for C being ( ( being_simple_closed_curve ) ( non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve ) Simple_closed_curve) holds UMP C : ( ( being_simple_closed_curve ) ( non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve with_the_max_arc ) Simple_closed_curve) : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Point of ( ( ) ( non empty V30() ) set ) ) <> LMP C : ( ( being_simple_closed_curve ) ( non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve with_the_max_arc ) Simple_closed_curve) : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Point of ( ( ) ( non empty V30() ) set ) ) ;

theorem :: JORDAN21:38
for C being ( ( being_simple_closed_curve ) ( non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve ) Simple_closed_curve) holds S-bound C : ( ( being_simple_closed_curve ) ( non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve with_the_max_arc ) Simple_closed_curve) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) < (UMP C : ( ( being_simple_closed_curve ) ( non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve with_the_max_arc ) Simple_closed_curve) ) : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Point of ( ( ) ( non empty V30() ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ;

theorem :: JORDAN21:39
for C being ( ( being_simple_closed_curve ) ( non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve ) Simple_closed_curve) holds (UMP C : ( ( being_simple_closed_curve ) ( non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve with_the_max_arc ) Simple_closed_curve) ) : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Point of ( ( ) ( non empty V30() ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) <= N-bound C : ( ( being_simple_closed_curve ) ( non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve with_the_max_arc ) Simple_closed_curve) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ;

theorem :: JORDAN21:40
for C being ( ( being_simple_closed_curve ) ( non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve ) Simple_closed_curve) holds S-bound C : ( ( being_simple_closed_curve ) ( non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve with_the_max_arc ) Simple_closed_curve) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) <= (LMP C : ( ( being_simple_closed_curve ) ( non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve with_the_max_arc ) Simple_closed_curve) ) : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Point of ( ( ) ( non empty V30() ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ;

theorem :: JORDAN21:41
for C being ( ( being_simple_closed_curve ) ( non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve ) Simple_closed_curve) holds (LMP C : ( ( being_simple_closed_curve ) ( non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve with_the_max_arc ) Simple_closed_curve) ) : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Point of ( ( ) ( non empty V30() ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) < N-bound C : ( ( being_simple_closed_curve ) ( non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve with_the_max_arc ) Simple_closed_curve) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ;

theorem :: JORDAN21:42
for C being ( ( being_simple_closed_curve ) ( non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve ) Simple_closed_curve) holds LSeg ((UMP C : ( ( being_simple_closed_curve ) ( non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve with_the_max_arc ) Simple_closed_curve) ) : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Point of ( ( ) ( non empty V30() ) set ) ) ,|[(((W-bound C : ( ( being_simple_closed_curve ) ( non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve with_the_max_arc ) Simple_closed_curve) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) + (E-bound C : ( ( being_simple_closed_curve ) ( non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve with_the_max_arc ) Simple_closed_curve) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) / 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ,(N-bound C : ( ( being_simple_closed_curve ) ( non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve with_the_max_arc ) Simple_closed_curve) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ]| : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) ) : ( ( ) ( non empty connected convex ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) : ( ( ) ( ) set ) ) misses LSeg ((LMP C : ( ( being_simple_closed_curve ) ( non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve with_the_max_arc ) Simple_closed_curve) ) : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Point of ( ( ) ( non empty V30() ) set ) ) ,|[(((W-bound C : ( ( being_simple_closed_curve ) ( non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve with_the_max_arc ) Simple_closed_curve) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) + (E-bound C : ( ( being_simple_closed_curve ) ( non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve with_the_max_arc ) Simple_closed_curve) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) / 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ,(S-bound C : ( ( being_simple_closed_curve ) ( non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve with_the_max_arc ) Simple_closed_curve) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ]| : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) ) : ( ( ) ( non empty connected convex ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: JORDAN21:43
for A, B being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) c= B : ( ( ) ( ) Subset of ) & (W-bound A : ( ( ) ( ) Subset of ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) + (E-bound A : ( ( ) ( ) Subset of ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) = (W-bound B : ( ( ) ( ) Subset of ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) + (E-bound B : ( ( ) ( ) Subset of ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) & not A : ( ( ) ( ) Subset of ) /\ (Vertical_Line (((W-bound A : ( ( ) ( ) Subset of ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) + (E-bound A : ( ( ) ( ) Subset of ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) / 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) : ( ( ) ( ) set ) ) is empty & proj2 : ( ( V27() V33( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) , REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ) ( V22() V25( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) V26( REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) V27() V33( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) , REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) V138() V139() V140() ) Element of K6(K7( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ,REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( V138() V139() V140() ) set ) ) : ( ( ) ( ) set ) ) .: (B : ( ( ) ( ) Subset of ) /\ (Vertical_Line (((W-bound A : ( ( ) ( ) Subset of ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) + (E-bound A : ( ( ) ( ) Subset of ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) / 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V148() V149() V150() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) is bounded_above holds
(UMP A : ( ( ) ( ) Subset of ) ) : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Point of ( ( ) ( non empty V30() ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) <= (UMP B : ( ( ) ( ) Subset of ) ) : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Point of ( ( ) ( non empty V30() ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ;

theorem :: JORDAN21:44
for A, B being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) c= B : ( ( ) ( ) Subset of ) & (W-bound A : ( ( ) ( ) Subset of ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) + (E-bound A : ( ( ) ( ) Subset of ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) = (W-bound B : ( ( ) ( ) Subset of ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) + (E-bound B : ( ( ) ( ) Subset of ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) & not A : ( ( ) ( ) Subset of ) /\ (Vertical_Line (((W-bound A : ( ( ) ( ) Subset of ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) + (E-bound A : ( ( ) ( ) Subset of ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) / 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) : ( ( ) ( ) set ) ) is empty & proj2 : ( ( V27() V33( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) , REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ) ( V22() V25( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) V26( REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) V27() V33( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) , REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) V138() V139() V140() ) Element of K6(K7( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ,REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( V138() V139() V140() ) set ) ) : ( ( ) ( ) set ) ) .: (B : ( ( ) ( ) Subset of ) /\ (Vertical_Line (((W-bound A : ( ( ) ( ) Subset of ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) + (E-bound A : ( ( ) ( ) Subset of ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) / 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V148() V149() V150() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) is bounded_below holds
(LMP B : ( ( ) ( ) Subset of ) ) : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Point of ( ( ) ( non empty V30() ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) <= (LMP A : ( ( ) ( ) Subset of ) ) : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Point of ( ( ) ( non empty V30() ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ;

theorem :: JORDAN21:45
for A, B being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) c= B : ( ( ) ( ) Subset of ) & UMP B : ( ( ) ( ) Subset of ) : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Point of ( ( ) ( non empty V30() ) set ) ) in A : ( ( ) ( ) Subset of ) & not A : ( ( ) ( ) Subset of ) /\ (Vertical_Line (((W-bound A : ( ( ) ( ) Subset of ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) + (E-bound A : ( ( ) ( ) Subset of ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) / 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) : ( ( ) ( ) set ) ) is empty & proj2 : ( ( V27() V33( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) , REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ) ( V22() V25( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) V26( REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) V27() V33( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) , REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) V138() V139() V140() ) Element of K6(K7( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ,REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( V138() V139() V140() ) set ) ) : ( ( ) ( ) set ) ) .: (B : ( ( ) ( ) Subset of ) /\ (Vertical_Line (((W-bound B : ( ( ) ( ) Subset of ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) + (E-bound B : ( ( ) ( ) Subset of ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) / 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V148() V149() V150() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) is bounded_above & (W-bound A : ( ( ) ( ) Subset of ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) + (E-bound A : ( ( ) ( ) Subset of ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) = (W-bound B : ( ( ) ( ) Subset of ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) + (E-bound B : ( ( ) ( ) Subset of ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) holds
UMP A : ( ( ) ( ) Subset of ) : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Point of ( ( ) ( non empty V30() ) set ) ) = UMP B : ( ( ) ( ) Subset of ) : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Point of ( ( ) ( non empty V30() ) set ) ) ;

theorem :: JORDAN21:46
for A, B being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) c= B : ( ( ) ( ) Subset of ) & LMP B : ( ( ) ( ) Subset of ) : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Point of ( ( ) ( non empty V30() ) set ) ) in A : ( ( ) ( ) Subset of ) & not A : ( ( ) ( ) Subset of ) /\ (Vertical_Line (((W-bound A : ( ( ) ( ) Subset of ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) + (E-bound A : ( ( ) ( ) Subset of ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) / 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) : ( ( ) ( ) set ) ) is empty & proj2 : ( ( V27() V33( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) , REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ) ( V22() V25( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) V26( REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) V27() V33( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) , REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) V138() V139() V140() ) Element of K6(K7( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ,REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( V138() V139() V140() ) set ) ) : ( ( ) ( ) set ) ) .: (B : ( ( ) ( ) Subset of ) /\ (Vertical_Line (((W-bound B : ( ( ) ( ) Subset of ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) + (E-bound B : ( ( ) ( ) Subset of ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) / 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V148() V149() V150() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) is bounded_below & (W-bound A : ( ( ) ( ) Subset of ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) + (E-bound A : ( ( ) ( ) Subset of ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) = (W-bound B : ( ( ) ( ) Subset of ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) + (E-bound B : ( ( ) ( ) Subset of ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) holds
LMP A : ( ( ) ( ) Subset of ) : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Point of ( ( ) ( non empty V30() ) set ) ) = LMP B : ( ( ) ( ) Subset of ) : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Point of ( ( ) ( non empty V30() ) set ) ) ;

theorem :: JORDAN21:47
for C being ( ( being_simple_closed_curve ) ( non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve ) Simple_closed_curve) holds (UMP (Upper_Arc C : ( ( being_simple_closed_curve ) ( non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve with_the_max_arc ) Simple_closed_curve) ) : ( ( non empty ) ( non empty closed compact bounded with_the_max_arc ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Point of ( ( ) ( non empty V30() ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) <= N-bound C : ( ( being_simple_closed_curve ) ( non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve with_the_max_arc ) Simple_closed_curve) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ;

theorem :: JORDAN21:48
for C being ( ( being_simple_closed_curve ) ( non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve ) Simple_closed_curve) holds S-bound C : ( ( being_simple_closed_curve ) ( non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve with_the_max_arc ) Simple_closed_curve) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) <= (LMP (Lower_Arc C : ( ( being_simple_closed_curve ) ( non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve with_the_max_arc ) Simple_closed_curve) ) : ( ( non empty ) ( non empty closed compact bounded with_the_max_arc ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Point of ( ( ) ( non empty V30() ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) ;

theorem :: JORDAN21:49
for C being ( ( being_simple_closed_curve ) ( non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve ) Simple_closed_curve) holds
( not LMP C : ( ( being_simple_closed_curve ) ( non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve with_the_max_arc ) Simple_closed_curve) : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Point of ( ( ) ( non empty V30() ) set ) ) in Lower_Arc C : ( ( being_simple_closed_curve ) ( non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve with_the_max_arc ) Simple_closed_curve) : ( ( non empty ) ( non empty closed compact bounded with_the_max_arc ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) : ( ( ) ( ) set ) ) or not UMP C : ( ( being_simple_closed_curve ) ( non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve with_the_max_arc ) Simple_closed_curve) : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Point of ( ( ) ( non empty V30() ) set ) ) in Lower_Arc C : ( ( being_simple_closed_curve ) ( non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve with_the_max_arc ) Simple_closed_curve) : ( ( non empty ) ( non empty closed compact bounded with_the_max_arc ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: JORDAN21:50
for C being ( ( being_simple_closed_curve ) ( non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve ) Simple_closed_curve) holds
( not LMP C : ( ( being_simple_closed_curve ) ( non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve with_the_max_arc ) Simple_closed_curve) : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Point of ( ( ) ( non empty V30() ) set ) ) in Upper_Arc C : ( ( being_simple_closed_curve ) ( non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve with_the_max_arc ) Simple_closed_curve) : ( ( non empty ) ( non empty closed compact bounded with_the_max_arc ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) : ( ( ) ( ) set ) ) or not UMP C : ( ( being_simple_closed_curve ) ( non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve with_the_max_arc ) Simple_closed_curve) : ( ( ) ( V43(2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) V97() V140() ) Point of ( ( ) ( non empty V30() ) set ) ) in Upper_Arc C : ( ( being_simple_closed_curve ) ( non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve with_the_max_arc ) Simple_closed_curve) : ( ( non empty ) ( non empty closed compact bounded with_the_max_arc ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_2 V114() V160() V161() V162() V163() V164() V165() V166() strict add-continuous Mult-continuous ) RLTopStruct ) : ( ( ) ( non empty V30() ) set ) ) : ( ( ) ( ) set ) ) ) ;