:: JGRAPH_8 semantic presentation

begin

registration
let a, b, c, d be ( ( real ) ( V11() real ext-real ) number ) ;
cluster closed_inside_of_rectangle (a : ( ( real ) ( V11() real ext-real ) set ) ,b : ( ( real ) ( V11() real ext-real ) set ) ,c : ( ( real ) ( V11() real ext-real ) set ) ,d : ( ( real ) ( V11() real ext-real ) set ) ) : ( ( ) ( functional ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) : ( ( ) ( ) set ) ) -> convex ;
end;

registration
let a, b, c, d be ( ( real ) ( V11() real ext-real ) number ) ;
cluster Trectangle (a : ( ( real ) ( V11() real ext-real ) set ) ,b : ( ( real ) ( V11() real ext-real ) set ) ,c : ( ( real ) ( V11() real ext-real ) set ) ,d : ( ( real ) ( V11() real ext-real ) set ) ) : ( ( ) ( TopSpace-like ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) ) -> convex ;
end;

theorem :: JGRAPH_8:1
for n being ( ( ) ( natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) )
for e being ( ( real positive ) ( non empty V11() real ext-real positive non negative ) number )
for g being ( ( Function-like V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V148() V149() V150() ) set ) , the carrier of (TOP-REAL b1 : ( ( ) ( natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) continuous ) ( non empty V22() V25( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V148() V149() V150() ) set ) ) V26( the carrier of (TOP-REAL b1 : ( ( ) ( natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) Function-like total V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V148() V149() V150() ) set ) , the carrier of (TOP-REAL b1 : ( ( ) ( natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) continuous ) Function of ( ( ) ( non empty V148() V149() V150() ) set ) , ( ( ) ( non empty functional ) set ) ) ex h being ( ( ) ( V22() V25( NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) V26( REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) Function-like V36() FinSequence-like FinSubsequence-like V138() V139() V140() ) FinSequence of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) st
( h : ( ( ) ( V22() V25( NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) V26( REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) Function-like V36() FinSequence-like FinSubsequence-like V138() V139() V140() ) FinSequence of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) . 1 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) = 0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V22() non-empty empty-yielding V25( NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) V26( RAT : ( ( ) ( non empty V36() V148() V149() V150() V151() V154() ) set ) ) Function-like one-to-one constant functional V36() FinSequence-like FinSubsequence-like FinSequence-membered integer V101() V138() V139() V140() V141() V148() V149() V150() V151() V152() V153() V154() V222() V223() V224() V225() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) & h : ( ( ) ( V22() V25( NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) V26( REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) Function-like V36() FinSequence-like FinSubsequence-like V138() V139() V140() ) FinSequence of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) . (len h : ( ( ) ( V22() V25( NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) V26( REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) Function-like V36() FinSequence-like FinSubsequence-like V138() V139() V140() ) FinSequence of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) ) : ( ( ) ( natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) = 1 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) & 5 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) <= len h : ( ( ) ( V22() V25( NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) V26( REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) Function-like V36() FinSequence-like FinSubsequence-like V138() V139() V140() ) FinSequence of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) & rng h : ( ( ) ( V22() V25( NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) V26( REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) Function-like V36() FinSequence-like FinSubsequence-like V138() V139() V140() ) FinSequence of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( V148() V149() V150() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) c= the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V148() V149() V150() ) set ) & h : ( ( ) ( V22() V25( NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) V26( REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) Function-like V36() FinSequence-like FinSubsequence-like V138() V139() V140() ) FinSequence of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) is increasing & ( for i being ( ( ) ( natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) )
for Q being ( ( ) ( V148() V149() V150() ) Subset of )
for W being ( ( ) ( ) Subset of ) st 1 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) <= i : ( ( ) ( natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) & i : ( ( ) ( natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) < len h : ( ( ) ( V22() V25( NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) V26( REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) Function-like V36() FinSequence-like FinSubsequence-like V138() V139() V140() ) FinSequence of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) & Q : ( ( ) ( V148() V149() V150() ) Subset of ) = [.(h : ( ( ) ( V22() V25( NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) V26( REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) Function-like V36() FinSequence-like FinSubsequence-like V138() V139() V140() ) FinSequence of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) /. i : ( ( ) ( natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) ,(h : ( ( ) ( V22() V25( NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) V26( REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) Function-like V36() FinSequence-like FinSubsequence-like V138() V139() V140() ) FinSequence of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) /. (i : ( ( ) ( natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) .] : ( ( ) ( compact V148() V149() V150() V225() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) & W : ( ( ) ( ) Subset of ) = g : ( ( Function-like V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V148() V149() V150() ) set ) , the carrier of (TOP-REAL b1 : ( ( ) ( natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) continuous ) ( non empty V22() V25( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V148() V149() V150() ) set ) ) V26( the carrier of (TOP-REAL b1 : ( ( ) ( natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) Function-like total V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V148() V149() V150() ) set ) , the carrier of (TOP-REAL b1 : ( ( ) ( natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) continuous ) Function of ( ( ) ( non empty V148() V149() V150() ) set ) , ( ( ) ( non empty functional ) set ) ) .: Q : ( ( ) ( V148() V149() V150() ) Subset of ) : ( ( ) ( functional ) Element of K6( the carrier of (TOP-REAL b1 : ( ( ) ( natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) : ( ( ) ( ) set ) ) holds
diameter W : ( ( ) ( ) Subset of ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) < e : ( ( real positive ) ( non empty V11() real ext-real positive non negative ) number ) ) ) ;

theorem :: JGRAPH_8:2
for n being ( ( ) ( natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) )
for p1, p2 being ( ( ) ( V22() V25( NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V36() V43(b1 : ( ( ) ( natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V138() V139() V140() ) Point of ( ( ) ( non empty functional ) set ) )
for P being ( ( ) ( functional ) Subset of ) st P : ( ( ) ( functional ) Subset of ) c= LSeg (p1 : ( ( ) ( V22() V25( NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V36() V43(b1 : ( ( ) ( natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V138() V139() V140() ) Point of ( ( ) ( non empty functional ) set ) ) ,p2 : ( ( ) ( V22() V25( NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V36() V43(b1 : ( ( ) ( natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V138() V139() V140() ) Point of ( ( ) ( non empty functional ) set ) ) ) : ( ( ) ( functional closed compact ) Element of K6( the carrier of (TOP-REAL b1 : ( ( ) ( natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) : ( ( ) ( ) set ) ) & p1 : ( ( ) ( V22() V25( NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V36() V43(b1 : ( ( ) ( natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V138() V139() V140() ) Point of ( ( ) ( non empty functional ) set ) ) in P : ( ( ) ( functional ) Subset of ) & p2 : ( ( ) ( V22() V25( NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V36() V43(b1 : ( ( ) ( natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V138() V139() V140() ) Point of ( ( ) ( non empty functional ) set ) ) in P : ( ( ) ( functional ) Subset of ) & P : ( ( ) ( functional ) Subset of ) is connected holds
P : ( ( ) ( functional ) Subset of ) = LSeg (p1 : ( ( ) ( V22() V25( NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V36() V43(b1 : ( ( ) ( natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V138() V139() V140() ) Point of ( ( ) ( non empty functional ) set ) ) ,p2 : ( ( ) ( V22() V25( NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V36() V43(b1 : ( ( ) ( natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V138() V139() V140() ) Point of ( ( ) ( non empty functional ) set ) ) ) : ( ( ) ( functional closed compact ) Element of K6( the carrier of (TOP-REAL b1 : ( ( ) ( natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: JGRAPH_8:3
for n being ( ( ) ( natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) )
for p1, p2 being ( ( ) ( V22() V25( NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V36() V43(b1 : ( ( ) ( natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V138() V139() V140() ) Point of ( ( ) ( non empty functional ) set ) )
for g being ( ( ) ( non empty V22() V25( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V210() ) TopStruct ) ) : ( ( ) ( non empty V148() V149() V150() ) set ) ) V26( the carrier of (TOP-REAL b1 : ( ( ) ( natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) Function-like total V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V210() ) TopStruct ) ) : ( ( ) ( non empty V148() V149() V150() ) set ) , the carrier of (TOP-REAL b1 : ( ( ) ( natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) continuous ) Path of p1 : ( ( ) ( V22() V25( NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V36() V43(b1 : ( ( ) ( natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V138() V139() V140() ) Point of ( ( ) ( non empty functional ) set ) ) ,p2 : ( ( ) ( V22() V25( NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V36() V43(b1 : ( ( ) ( natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V138() V139() V140() ) Point of ( ( ) ( non empty functional ) set ) ) ) st rng g : ( ( ) ( non empty V22() V25( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V210() ) TopStruct ) ) : ( ( ) ( non empty V148() V149() V150() ) set ) ) V26( the carrier of (TOP-REAL b1 : ( ( ) ( natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) Function-like total V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V210() ) TopStruct ) ) : ( ( ) ( non empty V148() V149() V150() ) set ) , the carrier of (TOP-REAL b1 : ( ( ) ( natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) continuous ) Path of b2 : ( ( ) ( V22() V25( NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V36() V43(b1 : ( ( ) ( natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V138() V139() V140() ) Point of ( ( ) ( non empty functional ) set ) ) ,b3 : ( ( ) ( V22() V25( NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V36() V43(b1 : ( ( ) ( natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V138() V139() V140() ) Point of ( ( ) ( non empty functional ) set ) ) ) : ( ( ) ( non empty functional ) Element of K6( the carrier of (TOP-REAL b1 : ( ( ) ( natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) : ( ( ) ( ) set ) ) c= LSeg (p1 : ( ( ) ( V22() V25( NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V36() V43(b1 : ( ( ) ( natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V138() V139() V140() ) Point of ( ( ) ( non empty functional ) set ) ) ,p2 : ( ( ) ( V22() V25( NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V36() V43(b1 : ( ( ) ( natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V138() V139() V140() ) Point of ( ( ) ( non empty functional ) set ) ) ) : ( ( ) ( functional closed compact ) Element of K6( the carrier of (TOP-REAL b1 : ( ( ) ( natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) : ( ( ) ( ) set ) ) holds
rng g : ( ( ) ( non empty V22() V25( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V210() ) TopStruct ) ) : ( ( ) ( non empty V148() V149() V150() ) set ) ) V26( the carrier of (TOP-REAL b1 : ( ( ) ( natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) Function-like total V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V210() ) TopStruct ) ) : ( ( ) ( non empty V148() V149() V150() ) set ) , the carrier of (TOP-REAL b1 : ( ( ) ( natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) continuous ) Path of b2 : ( ( ) ( V22() V25( NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V36() V43(b1 : ( ( ) ( natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V138() V139() V140() ) Point of ( ( ) ( non empty functional ) set ) ) ,b3 : ( ( ) ( V22() V25( NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V36() V43(b1 : ( ( ) ( natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V138() V139() V140() ) Point of ( ( ) ( non empty functional ) set ) ) ) : ( ( ) ( non empty functional ) Element of K6( the carrier of (TOP-REAL b1 : ( ( ) ( natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) : ( ( ) ( ) set ) ) = LSeg (p1 : ( ( ) ( V22() V25( NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V36() V43(b1 : ( ( ) ( natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V138() V139() V140() ) Point of ( ( ) ( non empty functional ) set ) ) ,p2 : ( ( ) ( V22() V25( NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V36() V43(b1 : ( ( ) ( natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V138() V139() V140() ) Point of ( ( ) ( non empty functional ) set ) ) ) : ( ( ) ( functional closed compact ) Element of K6( the carrier of (TOP-REAL b1 : ( ( ) ( natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: JGRAPH_8:4
for P, Q being ( ( non empty ) ( non empty functional ) Subset of )
for p1, p2, q1, q2 being ( ( ) ( V22() V25( NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V36() V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V138() V139() V140() ) Point of ( ( ) ( non empty functional ) set ) )
for f being ( ( ) ( non empty V22() V25( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V210() ) TopStruct ) ) : ( ( ) ( non empty V148() V149() V150() ) set ) ) V26( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) Function-like total V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V210() ) TopStruct ) ) : ( ( ) ( non empty V148() V149() V150() ) set ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) continuous ) Path of p1 : ( ( ) ( V22() V25( NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V36() V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V138() V139() V140() ) Point of ( ( ) ( non empty functional ) set ) ) ,p2 : ( ( ) ( V22() V25( NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V36() V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V138() V139() V140() ) Point of ( ( ) ( non empty functional ) set ) ) )
for g being ( ( ) ( non empty V22() V25( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V210() ) TopStruct ) ) : ( ( ) ( non empty V148() V149() V150() ) set ) ) V26( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) Function-like total V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V210() ) TopStruct ) ) : ( ( ) ( non empty V148() V149() V150() ) set ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) continuous ) Path of q1 : ( ( ) ( V22() V25( NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V36() V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V138() V139() V140() ) Point of ( ( ) ( non empty functional ) set ) ) ,q2 : ( ( ) ( V22() V25( NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V36() V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V138() V139() V140() ) Point of ( ( ) ( non empty functional ) set ) ) ) st rng f : ( ( ) ( non empty V22() V25( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V210() ) TopStruct ) ) : ( ( ) ( non empty V148() V149() V150() ) set ) ) V26( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) Function-like total V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V210() ) TopStruct ) ) : ( ( ) ( non empty V148() V149() V150() ) set ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) continuous ) Path of b3 : ( ( ) ( V22() V25( NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V36() V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V138() V139() V140() ) Point of ( ( ) ( non empty functional ) set ) ) ,b4 : ( ( ) ( V22() V25( NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V36() V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V138() V139() V140() ) Point of ( ( ) ( non empty functional ) set ) ) ) : ( ( ) ( non empty functional ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) : ( ( ) ( ) set ) ) = P : ( ( non empty ) ( non empty functional ) Subset of ) & rng g : ( ( ) ( non empty V22() V25( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V210() ) TopStruct ) ) : ( ( ) ( non empty V148() V149() V150() ) set ) ) V26( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) Function-like total V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V210() ) TopStruct ) ) : ( ( ) ( non empty V148() V149() V150() ) set ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) continuous ) Path of b5 : ( ( ) ( V22() V25( NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V36() V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V138() V139() V140() ) Point of ( ( ) ( non empty functional ) set ) ) ,b6 : ( ( ) ( V22() V25( NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V36() V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V138() V139() V140() ) Point of ( ( ) ( non empty functional ) set ) ) ) : ( ( ) ( non empty functional ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) : ( ( ) ( ) set ) ) = Q : ( ( non empty ) ( non empty functional ) Subset of ) & ( for p being ( ( ) ( V22() V25( NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V36() V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V138() V139() V140() ) Point of ( ( ) ( non empty functional ) set ) ) st p : ( ( ) ( V22() V25( NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V36() V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V138() V139() V140() ) Point of ( ( ) ( non empty functional ) set ) ) in P : ( ( non empty ) ( non empty functional ) Subset of ) holds
( p1 : ( ( ) ( V22() V25( NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V36() V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V138() V139() V140() ) Point of ( ( ) ( non empty functional ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) <= p : ( ( ) ( V22() V25( NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V36() V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V138() V139() V140() ) Point of ( ( ) ( non empty functional ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) & p : ( ( ) ( V22() V25( NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V36() V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V138() V139() V140() ) Point of ( ( ) ( non empty functional ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) <= p2 : ( ( ) ( V22() V25( NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V36() V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V138() V139() V140() ) Point of ( ( ) ( non empty functional ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) ) ) & ( for p being ( ( ) ( V22() V25( NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V36() V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V138() V139() V140() ) Point of ( ( ) ( non empty functional ) set ) ) st p : ( ( ) ( V22() V25( NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V36() V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V138() V139() V140() ) Point of ( ( ) ( non empty functional ) set ) ) in Q : ( ( non empty ) ( non empty functional ) Subset of ) holds
( p1 : ( ( ) ( V22() V25( NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V36() V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V138() V139() V140() ) Point of ( ( ) ( non empty functional ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) <= p : ( ( ) ( V22() V25( NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V36() V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V138() V139() V140() ) Point of ( ( ) ( non empty functional ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) & p : ( ( ) ( V22() V25( NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V36() V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V138() V139() V140() ) Point of ( ( ) ( non empty functional ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) <= p2 : ( ( ) ( V22() V25( NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V36() V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V138() V139() V140() ) Point of ( ( ) ( non empty functional ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) ) ) & ( for p being ( ( ) ( V22() V25( NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V36() V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V138() V139() V140() ) Point of ( ( ) ( non empty functional ) set ) ) st p : ( ( ) ( V22() V25( NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V36() V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V138() V139() V140() ) Point of ( ( ) ( non empty functional ) set ) ) in P : ( ( non empty ) ( non empty functional ) Subset of ) holds
( q1 : ( ( ) ( V22() V25( NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V36() V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V138() V139() V140() ) Point of ( ( ) ( non empty functional ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) <= p : ( ( ) ( V22() V25( NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V36() V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V138() V139() V140() ) Point of ( ( ) ( non empty functional ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) & p : ( ( ) ( V22() V25( NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V36() V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V138() V139() V140() ) Point of ( ( ) ( non empty functional ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) <= q2 : ( ( ) ( V22() V25( NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V36() V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V138() V139() V140() ) Point of ( ( ) ( non empty functional ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) ) ) & ( for p being ( ( ) ( V22() V25( NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V36() V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V138() V139() V140() ) Point of ( ( ) ( non empty functional ) set ) ) st p : ( ( ) ( V22() V25( NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V36() V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V138() V139() V140() ) Point of ( ( ) ( non empty functional ) set ) ) in Q : ( ( non empty ) ( non empty functional ) Subset of ) holds
( q1 : ( ( ) ( V22() V25( NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V36() V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V138() V139() V140() ) Point of ( ( ) ( non empty functional ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) <= p : ( ( ) ( V22() V25( NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V36() V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V138() V139() V140() ) Point of ( ( ) ( non empty functional ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) & p : ( ( ) ( V22() V25( NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V36() V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V138() V139() V140() ) Point of ( ( ) ( non empty functional ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) <= q2 : ( ( ) ( V22() V25( NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V36() V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V138() V139() V140() ) Point of ( ( ) ( non empty functional ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) ) ) holds
P : ( ( non empty ) ( non empty functional ) Subset of ) meets Q : ( ( non empty ) ( non empty functional ) Subset of ) ;

theorem :: JGRAPH_8:5
for a, b, c, d being ( ( real ) ( V11() real ext-real ) number )
for f, g being ( ( Function-like V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V148() V149() V150() ) set ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) continuous ) ( non empty V22() V25( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V148() V149() V150() ) set ) ) V26( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) Function-like total V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V148() V149() V150() ) set ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) continuous ) Function of ( ( ) ( non empty V148() V149() V150() ) set ) , ( ( ) ( non empty functional ) set ) )
for O, I being ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V148() V149() V150() ) set ) ) st O : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V148() V149() V150() ) set ) ) = 0 : ( ( ) ( empty natural V11() real ext-real non positive non negative V22() non-empty empty-yielding V25( NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) V26( RAT : ( ( ) ( non empty V36() V148() V149() V150() V151() V154() ) set ) ) Function-like one-to-one constant functional V36() FinSequence-like FinSubsequence-like FinSequence-membered integer V101() V138() V139() V140() V141() V148() V149() V150() V151() V152() V153() V154() V222() V223() V224() V225() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) & I : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V148() V149() V150() ) set ) ) = 1 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) & (f : ( ( Function-like V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V148() V149() V150() ) set ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) continuous ) ( non empty V22() V25( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V148() V149() V150() ) set ) ) V26( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) Function-like total V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V148() V149() V150() ) set ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) continuous ) Function of ( ( ) ( non empty V148() V149() V150() ) set ) , ( ( ) ( non empty functional ) set ) ) . O : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V148() V149() V150() ) set ) ) ) : ( ( ) ( V22() V25( NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V36() V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V138() V139() V140() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) = a : ( ( real ) ( V11() real ext-real ) number ) & (f : ( ( Function-like V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V148() V149() V150() ) set ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) continuous ) ( non empty V22() V25( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V148() V149() V150() ) set ) ) V26( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) Function-like total V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V148() V149() V150() ) set ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) continuous ) Function of ( ( ) ( non empty V148() V149() V150() ) set ) , ( ( ) ( non empty functional ) set ) ) . I : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V148() V149() V150() ) set ) ) ) : ( ( ) ( V22() V25( NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V36() V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V138() V139() V140() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) = b : ( ( real ) ( V11() real ext-real ) number ) & (g : ( ( Function-like V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V148() V149() V150() ) set ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) continuous ) ( non empty V22() V25( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V148() V149() V150() ) set ) ) V26( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) Function-like total V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V148() V149() V150() ) set ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) continuous ) Function of ( ( ) ( non empty V148() V149() V150() ) set ) , ( ( ) ( non empty functional ) set ) ) . O : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V148() V149() V150() ) set ) ) ) : ( ( ) ( V22() V25( NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V36() V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V138() V139() V140() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) = c : ( ( real ) ( V11() real ext-real ) number ) & (g : ( ( Function-like V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V148() V149() V150() ) set ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) continuous ) ( non empty V22() V25( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V148() V149() V150() ) set ) ) V26( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) Function-like total V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V148() V149() V150() ) set ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) continuous ) Function of ( ( ) ( non empty V148() V149() V150() ) set ) , ( ( ) ( non empty functional ) set ) ) . I : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V148() V149() V150() ) set ) ) ) : ( ( ) ( V22() V25( NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V36() V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V138() V139() V140() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) = d : ( ( real ) ( V11() real ext-real ) number ) & ( for r being ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V148() V149() V150() ) set ) ) holds
( a : ( ( real ) ( V11() real ext-real ) number ) <= (f : ( ( Function-like V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V148() V149() V150() ) set ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) continuous ) ( non empty V22() V25( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V148() V149() V150() ) set ) ) V26( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) Function-like total V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V148() V149() V150() ) set ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) continuous ) Function of ( ( ) ( non empty V148() V149() V150() ) set ) , ( ( ) ( non empty functional ) set ) ) . r : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V148() V149() V150() ) set ) ) ) : ( ( ) ( V22() V25( NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V36() V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V138() V139() V140() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) & (f : ( ( Function-like V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V148() V149() V150() ) set ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) continuous ) ( non empty V22() V25( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V148() V149() V150() ) set ) ) V26( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) Function-like total V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V148() V149() V150() ) set ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) continuous ) Function of ( ( ) ( non empty V148() V149() V150() ) set ) , ( ( ) ( non empty functional ) set ) ) . r : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V148() V149() V150() ) set ) ) ) : ( ( ) ( V22() V25( NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V36() V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V138() V139() V140() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) <= b : ( ( real ) ( V11() real ext-real ) number ) & a : ( ( real ) ( V11() real ext-real ) number ) <= (g : ( ( Function-like V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V148() V149() V150() ) set ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) continuous ) ( non empty V22() V25( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V148() V149() V150() ) set ) ) V26( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) Function-like total V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V148() V149() V150() ) set ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) continuous ) Function of ( ( ) ( non empty V148() V149() V150() ) set ) , ( ( ) ( non empty functional ) set ) ) . r : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V148() V149() V150() ) set ) ) ) : ( ( ) ( V22() V25( NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V36() V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V138() V139() V140() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) & (g : ( ( Function-like V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V148() V149() V150() ) set ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) continuous ) ( non empty V22() V25( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V148() V149() V150() ) set ) ) V26( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) Function-like total V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V148() V149() V150() ) set ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) continuous ) Function of ( ( ) ( non empty V148() V149() V150() ) set ) , ( ( ) ( non empty functional ) set ) ) . r : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V148() V149() V150() ) set ) ) ) : ( ( ) ( V22() V25( NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V36() V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V138() V139() V140() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) <= b : ( ( real ) ( V11() real ext-real ) number ) & c : ( ( real ) ( V11() real ext-real ) number ) <= (f : ( ( Function-like V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V148() V149() V150() ) set ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) continuous ) ( non empty V22() V25( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V148() V149() V150() ) set ) ) V26( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) Function-like total V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V148() V149() V150() ) set ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) continuous ) Function of ( ( ) ( non empty V148() V149() V150() ) set ) , ( ( ) ( non empty functional ) set ) ) . r : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V148() V149() V150() ) set ) ) ) : ( ( ) ( V22() V25( NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V36() V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V138() V139() V140() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) & (f : ( ( Function-like V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V148() V149() V150() ) set ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) continuous ) ( non empty V22() V25( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V148() V149() V150() ) set ) ) V26( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) Function-like total V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V148() V149() V150() ) set ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) continuous ) Function of ( ( ) ( non empty V148() V149() V150() ) set ) , ( ( ) ( non empty functional ) set ) ) . r : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V148() V149() V150() ) set ) ) ) : ( ( ) ( V22() V25( NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V36() V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V138() V139() V140() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) <= d : ( ( real ) ( V11() real ext-real ) number ) & c : ( ( real ) ( V11() real ext-real ) number ) <= (g : ( ( Function-like V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V148() V149() V150() ) set ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) continuous ) ( non empty V22() V25( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V148() V149() V150() ) set ) ) V26( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) Function-like total V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V148() V149() V150() ) set ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) continuous ) Function of ( ( ) ( non empty V148() V149() V150() ) set ) , ( ( ) ( non empty functional ) set ) ) . r : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V148() V149() V150() ) set ) ) ) : ( ( ) ( V22() V25( NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V36() V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V138() V139() V140() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) & (g : ( ( Function-like V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V148() V149() V150() ) set ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) continuous ) ( non empty V22() V25( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V148() V149() V150() ) set ) ) V26( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) Function-like total V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V148() V149() V150() ) set ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) continuous ) Function of ( ( ) ( non empty V148() V149() V150() ) set ) , ( ( ) ( non empty functional ) set ) ) . r : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V148() V149() V150() ) set ) ) ) : ( ( ) ( V22() V25( NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V36() V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V138() V139() V140() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) <= d : ( ( real ) ( V11() real ext-real ) number ) ) ) holds
rng f : ( ( Function-like V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V148() V149() V150() ) set ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) continuous ) ( non empty V22() V25( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V148() V149() V150() ) set ) ) V26( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) Function-like total V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V148() V149() V150() ) set ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) continuous ) Function of ( ( ) ( non empty V148() V149() V150() ) set ) , ( ( ) ( non empty functional ) set ) ) : ( ( ) ( non empty functional ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) : ( ( ) ( ) set ) ) meets rng g : ( ( Function-like V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V148() V149() V150() ) set ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) continuous ) ( non empty V22() V25( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V148() V149() V150() ) set ) ) V26( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) Function-like total V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V148() V149() V150() ) set ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) continuous ) Function of ( ( ) ( non empty V148() V149() V150() ) set ) , ( ( ) ( non empty functional ) set ) ) : ( ( ) ( non empty functional ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: JGRAPH_8:6
for a, b, c, d being ( ( real ) ( V11() real ext-real ) number )
for ar, br, cr, dr being ( ( ) ( ) Point of ( ( ) ( ) set ) )
for h being ( ( ) ( V22() V25( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V210() ) TopStruct ) ) : ( ( ) ( non empty V148() V149() V150() ) set ) ) V26( the carrier of (Trectangle (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) ,b3 : ( ( real ) ( V11() real ext-real ) number ) ,b4 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( ) ( TopSpace-like convex ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) ) : ( ( ) ( ) set ) ) Function-like V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V210() ) TopStruct ) ) : ( ( ) ( non empty V148() V149() V150() ) set ) , the carrier of (Trectangle (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) ,b3 : ( ( real ) ( V11() real ext-real ) number ) ,b4 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( ) ( TopSpace-like convex ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) ) : ( ( ) ( ) set ) ) ) Path of ar : ( ( ) ( ) Point of ( ( ) ( ) set ) ) ,br : ( ( ) ( ) Point of ( ( ) ( ) set ) ) )
for v being ( ( ) ( V22() V25( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V210() ) TopStruct ) ) : ( ( ) ( non empty V148() V149() V150() ) set ) ) V26( the carrier of (Trectangle (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) ,b3 : ( ( real ) ( V11() real ext-real ) number ) ,b4 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( ) ( TopSpace-like convex ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) ) : ( ( ) ( ) set ) ) Function-like V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V210() ) TopStruct ) ) : ( ( ) ( non empty V148() V149() V150() ) set ) , the carrier of (Trectangle (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) ,b3 : ( ( real ) ( V11() real ext-real ) number ) ,b4 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( ) ( TopSpace-like convex ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) ) : ( ( ) ( ) set ) ) ) Path of dr : ( ( ) ( ) Point of ( ( ) ( ) set ) ) ,cr : ( ( ) ( ) Point of ( ( ) ( ) set ) ) )
for Ar, Br, Cr, Dr being ( ( ) ( V22() V25( NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V36() V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V138() V139() V140() ) Point of ( ( ) ( non empty functional ) set ) ) st Ar : ( ( ) ( V22() V25( NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V36() V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V138() V139() V140() ) Point of ( ( ) ( non empty functional ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) = a : ( ( real ) ( V11() real ext-real ) number ) & Br : ( ( ) ( V22() V25( NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V36() V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V138() V139() V140() ) Point of ( ( ) ( non empty functional ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) = b : ( ( real ) ( V11() real ext-real ) number ) & Cr : ( ( ) ( V22() V25( NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V36() V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V138() V139() V140() ) Point of ( ( ) ( non empty functional ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) = c : ( ( real ) ( V11() real ext-real ) number ) & Dr : ( ( ) ( V22() V25( NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V36() V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V138() V139() V140() ) Point of ( ( ) ( non empty functional ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) = d : ( ( real ) ( V11() real ext-real ) number ) & ar : ( ( ) ( ) Point of ( ( ) ( ) set ) ) = Ar : ( ( ) ( V22() V25( NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V36() V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V138() V139() V140() ) Point of ( ( ) ( non empty functional ) set ) ) & br : ( ( ) ( ) Point of ( ( ) ( ) set ) ) = Br : ( ( ) ( V22() V25( NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V36() V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V138() V139() V140() ) Point of ( ( ) ( non empty functional ) set ) ) & cr : ( ( ) ( ) Point of ( ( ) ( ) set ) ) = Cr : ( ( ) ( V22() V25( NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V36() V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V138() V139() V140() ) Point of ( ( ) ( non empty functional ) set ) ) & dr : ( ( ) ( ) Point of ( ( ) ( ) set ) ) = Dr : ( ( ) ( V22() V25( NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V36() V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V138() V139() V140() ) Point of ( ( ) ( non empty functional ) set ) ) holds
ex s, t being ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V148() V149() V150() ) set ) ) st h : ( ( ) ( V22() V25( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V210() ) TopStruct ) ) : ( ( ) ( non empty V148() V149() V150() ) set ) ) V26( the carrier of (Trectangle (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) ,b3 : ( ( real ) ( V11() real ext-real ) number ) ,b4 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( ) ( TopSpace-like convex ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) ) : ( ( ) ( ) set ) ) Function-like V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V210() ) TopStruct ) ) : ( ( ) ( non empty V148() V149() V150() ) set ) , the carrier of (Trectangle (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) ,b3 : ( ( real ) ( V11() real ext-real ) number ) ,b4 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( ) ( TopSpace-like convex ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) ) : ( ( ) ( ) set ) ) ) Path of b5 : ( ( ) ( ) Point of ( ( ) ( ) set ) ) ,b6 : ( ( ) ( ) Point of ( ( ) ( ) set ) ) ) . s : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V148() V149() V150() ) set ) ) : ( ( ) ( ) Element of the carrier of (Trectangle (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) ,b3 : ( ( real ) ( V11() real ext-real ) number ) ,b4 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( ) ( TopSpace-like convex ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) ) : ( ( ) ( ) set ) ) = v : ( ( ) ( V22() V25( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V210() ) TopStruct ) ) : ( ( ) ( non empty V148() V149() V150() ) set ) ) V26( the carrier of (Trectangle (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) ,b3 : ( ( real ) ( V11() real ext-real ) number ) ,b4 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( ) ( TopSpace-like convex ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) ) : ( ( ) ( ) set ) ) Function-like V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V210() ) TopStruct ) ) : ( ( ) ( non empty V148() V149() V150() ) set ) , the carrier of (Trectangle (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) ,b3 : ( ( real ) ( V11() real ext-real ) number ) ,b4 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( ) ( TopSpace-like convex ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) ) : ( ( ) ( ) set ) ) ) Path of b8 : ( ( ) ( ) Point of ( ( ) ( ) set ) ) ,b7 : ( ( ) ( ) Point of ( ( ) ( ) set ) ) ) . t : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V148() V149() V150() ) set ) ) : ( ( ) ( ) Element of the carrier of (Trectangle (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) ,b3 : ( ( real ) ( V11() real ext-real ) number ) ,b4 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( ) ( TopSpace-like convex ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) ) : ( ( ) ( ) set ) ) ;