TOPREAL5

:: TOPREAL5 semantic presentation

begin

for X being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for A, B1, B2 being ( ( ) ( ) Subset of ) st B1 : ( ( ) ( ) Subset of ) is open & B2 : ( ( ) ( ) Subset of ) is open & B1 : ( ( ) ( ) Subset of ) meets A : ( ( ) ( ) Subset of ) & B2 : ( ( ) ( ) Subset of ) meets A : ( ( ) ( ) Subset of ) & A : ( ( ) ( ) Subset of ) c= B1 : ( ( ) ( ) Subset of ) \/ B2 : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K6( the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) & B1 : ( ( ) ( ) Subset of ) misses B2 : ( ( ) ( ) Subset of ) holds
not A : ( ( ) ( ) Subset of ) is connected ;

theorem :: TOPREAL5:2

for ra, rb being ( ( real ) ( V11() real ext-real ) number ) st ra : ( ( real ) ( V11() real ext-real ) number ) <= rb : ( ( real ) ( V11() real ext-real ) number ) holds
[#] (Closed-Interval-TSpace (ra : ( ( real ) ( V11() real ext-real ) number ) ,rb : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty non proper closed V166() V167() V168() ) Element of K6( the carrier of (Closed-Interval-TSpace (b₁ : ( ( real ) ( V11() real ext-real ) number ) ,b₂ : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) ) : ( ( ) ( ) set ) ) is connected ;

theorem :: TOPREAL5:3

for A being ( ( ) ( V166() V167() V168() ) Subset of )
for a being ( ( real ) ( V11() real ext-real ) number ) st not a : ( ( real ) ( V11() real ext-real ) number ) in A : ( ( ) ( V166() V167() V168() ) Subset of ) & ex b, d being ( ( real ) ( V11() real ext-real ) number ) st
( b : ( ( real ) ( V11() real ext-real ) number ) in A : ( ( ) ( V166() V167() V168() ) Subset of ) & d : ( ( real ) ( V11() real ext-real ) number ) in A : ( ( ) ( V166() V167() V168() ) Subset of ) & b : ( ( real ) ( V11() real ext-real ) number ) < a : ( ( real ) ( V11() real ext-real ) number ) & a : ( ( real ) ( V11() real ext-real ) number ) < d : ( ( real ) ( V11() real ext-real ) number ) ) holds
not A : ( ( ) ( V166() V167() V168() ) Subset of ) is connected ;

theorem :: TOPREAL5:4

for X being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for xa, xb being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) )
for a, b, d being ( ( ) ( V11() real ext-real ) Real)
for f being ( ( Function-like V33( the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) ) continuous ) ( non empty Relation-like the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) -valued Function-like total V33( the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) ) continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty V166() V167() V168() ) set ) ) st X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) is connected & f : ( ( Function-like V33( the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) ) continuous ) ( non empty Relation-like the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) -valued Function-like total V33( the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) ) continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty V166() V167() V168() ) set ) ) . xa : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) = a : ( ( ) ( V11() real ext-real ) Real) & f : ( ( Function-like V33( the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) ) continuous ) ( non empty Relation-like the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) -valued Function-like total V33( the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) ) continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty V166() V167() V168() ) set ) ) . xb : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) = b : ( ( ) ( V11() real ext-real ) Real) & a : ( ( ) ( V11() real ext-real ) Real) <= d : ( ( ) ( V11() real ext-real ) Real) & d : ( ( ) ( V11() real ext-real ) Real) <= b : ( ( ) ( V11() real ext-real ) Real) holds
ex xc being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) st f : ( ( Function-like V33( the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) ) continuous ) ( non empty Relation-like the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) -valued Function-like total V33( the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) ) continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty V166() V167() V168() ) set ) ) . xc : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) = d : ( ( ) ( V11() real ext-real ) Real) ;

theorem :: TOPREAL5:5

for X being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for xa, xb being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) )
for B being ( ( ) ( ) Subset of )
for a, b, d being ( ( ) ( V11() real ext-real ) Real)
for f being ( ( Function-like V33( the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) ) continuous ) ( non empty Relation-like the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) -valued Function-like total V33( the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) ) continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty V166() V167() V168() ) set ) ) st B : ( ( ) ( ) Subset of ) is connected & f : ( ( Function-like V33( the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) ) continuous ) ( non empty Relation-like the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) -valued Function-like total V33( the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) ) continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty V166() V167() V168() ) set ) ) . xa : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) = a : ( ( ) ( V11() real ext-real ) Real) & f : ( ( Function-like V33( the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) ) continuous ) ( non empty Relation-like the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) -valued Function-like total V33( the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) ) continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty V166() V167() V168() ) set ) ) . xb : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) = b : ( ( ) ( V11() real ext-real ) Real) & a : ( ( ) ( V11() real ext-real ) Real) <= d : ( ( ) ( V11() real ext-real ) Real) & d : ( ( ) ( V11() real ext-real ) Real) <= b : ( ( ) ( V11() real ext-real ) Real) & xa : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) in B : ( ( ) ( ) Subset of ) & xb : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) in B : ( ( ) ( ) Subset of ) holds
ex xc being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) st
( xc : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) in B : ( ( ) ( ) Subset of ) & f : ( ( Function-like V33( the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) ) continuous ) ( non empty Relation-like the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) -valued Function-like total V33( the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) ) continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty V166() V167() V168() ) set ) ) . xc : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) = d : ( ( ) ( V11() real ext-real ) Real) ) ;

theorem :: TOPREAL5:6

for ra, rb, a, b being ( ( real ) ( V11() real ext-real ) number ) st ra : ( ( real ) ( V11() real ext-real ) number ) < rb : ( ( real ) ( V11() real ext-real ) number ) holds
for f being ( ( Function-like V33( the carrier of (Closed-Interval-TSpace (b₁ : ( ( real ) ( V11() real ext-real ) number ) ,b₂ : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) , the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) ) continuous ) ( non empty Relation-like the carrier of (Closed-Interval-TSpace (b₁ : ( ( real ) ( V11() real ext-real ) number ) ,b₂ : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) -valued Function-like total V33( the carrier of (Closed-Interval-TSpace (b₁ : ( ( real ) ( V11() real ext-real ) number ) ,b₂ : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) , the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) ) continuous ) Function of ( ( ) ( non empty V166() V167() V168() ) set ) , ( ( ) ( non empty V166() V167() V168() ) set ) )
for d being ( ( real ) ( V11() real ext-real ) number ) st f : ( ( Function-like V33( the carrier of (Closed-Interval-TSpace (b₁ : ( ( real ) ( V11() real ext-real ) number ) ,b₂ : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) , the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) ) continuous ) ( non empty Relation-like the carrier of (Closed-Interval-TSpace (b₁ : ( ( real ) ( V11() real ext-real ) number ) ,b₂ : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) -valued Function-like total V33( the carrier of (Closed-Interval-TSpace (b₁ : ( ( real ) ( V11() real ext-real ) number ) ,b₂ : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) , the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) ) continuous ) Function of ( ( ) ( non empty V166() V167() V168() ) set ) , ( ( ) ( non empty V166() V167() V168() ) set ) ) . ra : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( ) set ) = a : ( ( real ) ( V11() real ext-real ) number ) & f : ( ( Function-like V33( the carrier of (Closed-Interval-TSpace (b₁ : ( ( real ) ( V11() real ext-real ) number ) ,b₂ : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) , the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) ) continuous ) ( non empty Relation-like the carrier of (Closed-Interval-TSpace (b₁ : ( ( real ) ( V11() real ext-real ) number ) ,b₂ : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) -valued Function-like total V33( the carrier of (Closed-Interval-TSpace (b₁ : ( ( real ) ( V11() real ext-real ) number ) ,b₂ : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) , the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) ) continuous ) Function of ( ( ) ( non empty V166() V167() V168() ) set ) , ( ( ) ( non empty V166() V167() V168() ) set ) ) . rb : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( ) set ) = b : ( ( real ) ( V11() real ext-real ) number ) & a : ( ( real ) ( V11() real ext-real ) number ) < d : ( ( real ) ( V11() real ext-real ) number ) & d : ( ( real ) ( V11() real ext-real ) number ) < b : ( ( real ) ( V11() real ext-real ) number ) holds
ex rc being ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) st
( f : ( ( Function-like V33( the carrier of (Closed-Interval-TSpace (b₁ : ( ( real ) ( V11() real ext-real ) number ) ,b₂ : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) , the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) ) continuous ) ( non empty Relation-like the carrier of (Closed-Interval-TSpace (b₁ : ( ( real ) ( V11() real ext-real ) number ) ,b₂ : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) -valued Function-like total V33( the carrier of (Closed-Interval-TSpace (b₁ : ( ( real ) ( V11() real ext-real ) number ) ,b₂ : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) , the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) ) continuous ) Function of ( ( ) ( non empty V166() V167() V168() ) set ) , ( ( ) ( non empty V166() V167() V168() ) set ) ) . rc : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) = d : ( ( real ) ( V11() real ext-real ) number ) & ra : ( ( real ) ( V11() real ext-real ) number ) < rc : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) & rc : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) < rb : ( ( real ) ( V11() real ext-real ) number ) ) ;

theorem :: TOPREAL5:7

for ra, rb, a, b being ( ( real ) ( V11() real ext-real ) number ) st ra : ( ( real ) ( V11() real ext-real ) number ) < rb : ( ( real ) ( V11() real ext-real ) number ) holds
for f being ( ( Function-like V33( the carrier of (Closed-Interval-TSpace (b₁ : ( ( real ) ( V11() real ext-real ) number ) ,b₂ : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) , the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) ) continuous ) ( non empty Relation-like the carrier of (Closed-Interval-TSpace (b₁ : ( ( real ) ( V11() real ext-real ) number ) ,b₂ : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) -valued Function-like total V33( the carrier of (Closed-Interval-TSpace (b₁ : ( ( real ) ( V11() real ext-real ) number ) ,b₂ : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) , the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) ) continuous ) Function of ( ( ) ( non empty V166() V167() V168() ) set ) , ( ( ) ( non empty V166() V167() V168() ) set ) )
for d being ( ( real ) ( V11() real ext-real ) number ) st f : ( ( Function-like V33( the carrier of (Closed-Interval-TSpace (b₁ : ( ( real ) ( V11() real ext-real ) number ) ,b₂ : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) , the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) ) continuous ) ( non empty Relation-like the carrier of (Closed-Interval-TSpace (b₁ : ( ( real ) ( V11() real ext-real ) number ) ,b₂ : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) -valued Function-like total V33( the carrier of (Closed-Interval-TSpace (b₁ : ( ( real ) ( V11() real ext-real ) number ) ,b₂ : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) , the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) ) continuous ) Function of ( ( ) ( non empty V166() V167() V168() ) set ) , ( ( ) ( non empty V166() V167() V168() ) set ) ) . ra : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( ) set ) = a : ( ( real ) ( V11() real ext-real ) number ) & f : ( ( Function-like V33( the carrier of (Closed-Interval-TSpace (b₁ : ( ( real ) ( V11() real ext-real ) number ) ,b₂ : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) , the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) ) continuous ) ( non empty Relation-like the carrier of (Closed-Interval-TSpace (b₁ : ( ( real ) ( V11() real ext-real ) number ) ,b₂ : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) -valued Function-like total V33( the carrier of (Closed-Interval-TSpace (b₁ : ( ( real ) ( V11() real ext-real ) number ) ,b₂ : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) , the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) ) continuous ) Function of ( ( ) ( non empty V166() V167() V168() ) set ) , ( ( ) ( non empty V166() V167() V168() ) set ) ) . rb : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( ) set ) = b : ( ( real ) ( V11() real ext-real ) number ) & a : ( ( real ) ( V11() real ext-real ) number ) > d : ( ( real ) ( V11() real ext-real ) number ) & d : ( ( real ) ( V11() real ext-real ) number ) > b : ( ( real ) ( V11() real ext-real ) number ) holds
ex rc being ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) st
( f : ( ( Function-like V33( the carrier of (Closed-Interval-TSpace (b₁ : ( ( real ) ( V11() real ext-real ) number ) ,b₂ : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) , the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) ) continuous ) ( non empty Relation-like the carrier of (Closed-Interval-TSpace (b₁ : ( ( real ) ( V11() real ext-real ) number ) ,b₂ : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) -valued Function-like total V33( the carrier of (Closed-Interval-TSpace (b₁ : ( ( real ) ( V11() real ext-real ) number ) ,b₂ : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) , the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) ) continuous ) Function of ( ( ) ( non empty V166() V167() V168() ) set ) , ( ( ) ( non empty V166() V167() V168() ) set ) ) . rc : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) = d : ( ( real ) ( V11() real ext-real ) number ) & ra : ( ( real ) ( V11() real ext-real ) number ) < rc : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) & rc : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) < rb : ( ( real ) ( V11() real ext-real ) number ) ) ;

theorem :: TOPREAL5:8

for ra, rb being ( ( real ) ( V11() real ext-real ) number )
for g being ( ( Function-like V33( the carrier of (Closed-Interval-TSpace (b₁ : ( ( real ) ( V11() real ext-real ) number ) ,b₂ : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) , the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) ) continuous ) ( non empty Relation-like the carrier of (Closed-Interval-TSpace (b₁ : ( ( real ) ( V11() real ext-real ) number ) ,b₂ : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) -valued Function-like total V33( the carrier of (Closed-Interval-TSpace (b₁ : ( ( real ) ( V11() real ext-real ) number ) ,b₂ : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) , the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) ) continuous ) Function of ( ( ) ( non empty V166() V167() V168() ) set ) , ( ( ) ( non empty V166() V167() V168() ) set ) )
for s1, s2 being ( ( real ) ( V11() real ext-real ) number ) st ra : ( ( real ) ( V11() real ext-real ) number ) < rb : ( ( real ) ( V11() real ext-real ) number ) & s1 : ( ( real ) ( V11() real ext-real ) number ) * s2 : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( V11() real ext-real ) set ) < 0 : ( ( ) ( empty natural V11() real ext-real V118() V119() V166() V167() V168() V169() V170() V171() V172() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) & s1 : ( ( real ) ( V11() real ext-real ) number ) = g : ( ( Function-like V33( the carrier of (Closed-Interval-TSpace (b₁ : ( ( real ) ( V11() real ext-real ) number ) ,b₂ : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) , the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) ) continuous ) ( non empty Relation-like the carrier of (Closed-Interval-TSpace (b₁ : ( ( real ) ( V11() real ext-real ) number ) ,b₂ : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) -valued Function-like total V33( the carrier of (Closed-Interval-TSpace (b₁ : ( ( real ) ( V11() real ext-real ) number ) ,b₂ : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) , the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) ) continuous ) Function of ( ( ) ( non empty V166() V167() V168() ) set ) , ( ( ) ( non empty V166() V167() V168() ) set ) ) . ra : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( ) set ) & s2 : ( ( real ) ( V11() real ext-real ) number ) = g : ( ( Function-like V33( the carrier of (Closed-Interval-TSpace (b₁ : ( ( real ) ( V11() real ext-real ) number ) ,b₂ : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) , the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) ) continuous ) ( non empty Relation-like the carrier of (Closed-Interval-TSpace (b₁ : ( ( real ) ( V11() real ext-real ) number ) ,b₂ : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) -valued Function-like total V33( the carrier of (Closed-Interval-TSpace (b₁ : ( ( real ) ( V11() real ext-real ) number ) ,b₂ : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) , the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) ) continuous ) Function of ( ( ) ( non empty V166() V167() V168() ) set ) , ( ( ) ( non empty V166() V167() V168() ) set ) ) . rb : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( ) set ) holds
ex r1 being ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) st
( g : ( ( Function-like V33( the carrier of (Closed-Interval-TSpace (b₁ : ( ( real ) ( V11() real ext-real ) number ) ,b₂ : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) , the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) ) continuous ) ( non empty Relation-like the carrier of (Closed-Interval-TSpace (b₁ : ( ( real ) ( V11() real ext-real ) number ) ,b₂ : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) -valued Function-like total V33( the carrier of (Closed-Interval-TSpace (b₁ : ( ( real ) ( V11() real ext-real ) number ) ,b₂ : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) , the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) ) continuous ) Function of ( ( ) ( non empty V166() V167() V168() ) set ) , ( ( ) ( non empty V166() V167() V168() ) set ) ) . r1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) = 0 : ( ( ) ( empty natural V11() real ext-real V118() V119() V166() V167() V168() V169() V170() V171() V172() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) & ra : ( ( real ) ( V11() real ext-real ) number ) < r1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) & r1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) < rb : ( ( real ) ( V11() real ext-real ) number ) ) ;

theorem :: TOPREAL5:9

for g being ( ( Function-like V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) , the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) ) ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) -valued Function-like total V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) , the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) ) ) Function of ( ( ) ( non empty V166() V167() V168() ) set ) , ( ( ) ( non empty V166() V167() V168() ) set ) )
for s1, s2 being ( ( real ) ( V11() real ext-real ) number ) st g : ( ( Function-like V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) , the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) ) ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) -valued Function-like total V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) , the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) ) ) Function of ( ( ) ( non empty V166() V167() V168() ) set ) , ( ( ) ( non empty V166() V167() V168() ) set ) ) is continuous & g : ( ( Function-like V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) , the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) ) ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) -valued Function-like total V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) , the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) ) ) Function of ( ( ) ( non empty V166() V167() V168() ) set ) , ( ( ) ( non empty V166() V167() V168() ) set ) ) . 0 : ( ( ) ( empty natural V11() real ext-real V118() V119() V166() V167() V168() V169() V170() V171() V172() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) <> g : ( ( Function-like V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) , the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) ) ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) -valued Function-like total V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) , the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) ) ) Function of ( ( ) ( non empty V166() V167() V168() ) set ) , ( ( ) ( non empty V166() V167() V168() ) set ) ) . 1 : ( ( ) ( non empty natural V11() real ext-real positive V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) & s1 : ( ( real ) ( V11() real ext-real ) number ) = g : ( ( Function-like V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) , the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) ) ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) -valued Function-like total V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) , the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) ) ) Function of ( ( ) ( non empty V166() V167() V168() ) set ) , ( ( ) ( non empty V166() V167() V168() ) set ) ) . 0 : ( ( ) ( empty natural V11() real ext-real V118() V119() V166() V167() V168() V169() V170() V171() V172() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) & s2 : ( ( real ) ( V11() real ext-real ) number ) = g : ( ( Function-like V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) , the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) ) ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) -valued Function-like total V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) , the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) ) ) Function of ( ( ) ( non empty V166() V167() V168() ) set ) , ( ( ) ( non empty V166() V167() V168() ) set ) ) . 1 : ( ( ) ( non empty natural V11() real ext-real positive V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) holds
ex r1 being ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) st
( 0 : ( ( ) ( empty natural V11() real ext-real V118() V119() V166() V167() V168() V169() V170() V171() V172() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) < r1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) & r1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) < 1 : ( ( ) ( non empty natural V11() real ext-real positive V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) & g : ( ( Function-like V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) , the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) ) ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) -valued Function-like total V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) , the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) ) ) Function of ( ( ) ( non empty V166() V167() V168() ) set ) , ( ( ) ( non empty V166() V167() V168() ) set ) ) . r1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) = (s1 : ( ( real ) ( V11() real ext-real ) number ) + s2 : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) set ) / 2 : ( ( ) ( non empty natural V11() real ext-real positive V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) ) ;

begin

theorem :: TOPREAL5:10

for f being ( ( Function-like V33( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() V226() V227() ) L15()) : ( ( ) ( non empty ) set ) , the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) ) ) ( non empty Relation-like the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() V226() V227() ) L15()) : ( ( ) ( non empty ) set ) -defined the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) -valued Function-like total V33( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() V226() V227() ) L15()) : ( ( ) ( non empty ) set ) , the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty V166() V167() V168() ) set ) ) st f : ( ( Function-like V33( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() V226() V227() ) L15()) : ( ( ) ( non empty ) set ) , the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) ) ) ( non empty Relation-like the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() V226() V227() ) L15()) : ( ( ) ( non empty ) set ) -defined the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) -valued Function-like total V33( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() V226() V227() ) L15()) : ( ( ) ( non empty ) set ) , the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty V166() V167() V168() ) set ) ) = proj1 : ( ( Function-like V33( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() V226() V227() ) L15()) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) ) ( non empty Relation-like the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() V226() V227() ) L15()) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) -valued Function-like total V33( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() V226() V227() ) L15()) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) ) Element of K6(K7( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() V226() V227() ) L15()) : ( ( ) ( non empty ) set ) ,REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) holds
f : ( ( Function-like V33( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() V226() V227() ) L15()) : ( ( ) ( non empty ) set ) , the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) ) ) ( non empty Relation-like the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() V226() V227() ) L15()) : ( ( ) ( non empty ) set ) -defined the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) -valued Function-like total V33( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() V226() V227() ) L15()) : ( ( ) ( non empty ) set ) , the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty V166() V167() V168() ) set ) ) is continuous ;

theorem :: TOPREAL5:11

for f being ( ( Function-like V33( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() V226() V227() ) L15()) : ( ( ) ( non empty ) set ) , the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) ) ) ( non empty Relation-like the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() V226() V227() ) L15()) : ( ( ) ( non empty ) set ) -defined the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) -valued Function-like total V33( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() V226() V227() ) L15()) : ( ( ) ( non empty ) set ) , the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty V166() V167() V168() ) set ) ) st f : ( ( Function-like V33( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() V226() V227() ) L15()) : ( ( ) ( non empty ) set ) , the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) ) ) ( non empty Relation-like the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() V226() V227() ) L15()) : ( ( ) ( non empty ) set ) -defined the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) -valued Function-like total V33( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() V226() V227() ) L15()) : ( ( ) ( non empty ) set ) , the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty V166() V167() V168() ) set ) ) = proj2 : ( ( Function-like V33( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() V226() V227() ) L15()) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) ) ( non empty Relation-like the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() V226() V227() ) L15()) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) -valued Function-like total V33( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() V226() V227() ) L15()) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) ) Element of K6(K7( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() V226() V227() ) L15()) : ( ( ) ( non empty ) set ) ,REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) holds
f : ( ( Function-like V33( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() V226() V227() ) L15()) : ( ( ) ( non empty ) set ) , the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) ) ) ( non empty Relation-like the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() V226() V227() ) L15()) : ( ( ) ( non empty ) set ) -defined the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) -valued Function-like total V33( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() V226() V227() ) L15()) : ( ( ) ( non empty ) set ) , the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty V166() V167() V168() ) set ) ) is continuous ;

theorem :: TOPREAL5:12

for P being ( ( non empty ) ( non empty ) Subset of )
for f being ( ( Function-like V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) , the carrier of ((TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() V226() V227() ) L15()) | b₁ : ( ( non empty ) ( non empty ) Subset of ) ) : ( ( strict ) ( non empty strict TopSpace-like ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() V226() V227() ) L15()) ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of ((TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() V226() V227() ) L15()) | b₁ : ( ( non empty ) ( non empty ) Subset of ) ) : ( ( strict ) ( non empty strict TopSpace-like ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() V226() V227() ) L15()) ) : ( ( ) ( non empty ) set ) -valued Function-like total V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) , the carrier of ((TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() V226() V227() ) L15()) | b₁ : ( ( non empty ) ( non empty ) Subset of ) ) : ( ( strict ) ( non empty strict TopSpace-like ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() V226() V227() ) L15()) ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty V166() V167() V168() ) set ) , ( ( ) ( non empty ) set ) ) st f : ( ( Function-like V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) , the carrier of ((TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() V226() V227() ) L15()) | b₁ : ( ( non empty ) ( non empty ) Subset of ) ) : ( ( strict ) ( non empty strict TopSpace-like ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() V226() V227() ) L15()) ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of ((TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() V226() V227() ) L15()) | b₁ : ( ( non empty ) ( non empty ) Subset of ) ) : ( ( strict ) ( non empty strict TopSpace-like ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() V226() V227() ) L15()) ) : ( ( ) ( non empty ) set ) -valued Function-like total V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) , the carrier of ((TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() V226() V227() ) L15()) | b₁ : ( ( non empty ) ( non empty ) Subset of ) ) : ( ( strict ) ( non empty strict TopSpace-like ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() V226() V227() ) L15()) ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty V166() V167() V168() ) set ) , ( ( ) ( non empty ) set ) ) is continuous holds
ex g being ( ( Function-like V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) , the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) ) ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) -valued Function-like total V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) , the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) ) ) Function of ( ( ) ( non empty V166() V167() V168() ) set ) , ( ( ) ( non empty V166() V167() V168() ) set ) ) st
( g : ( ( Function-like V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) , the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) ) ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) -valued Function-like total V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) , the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) ) ) Function of ( ( ) ( non empty V166() V167() V168() ) set ) , ( ( ) ( non empty V166() V167() V168() ) set ) ) is continuous & ( for r being ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) )
for q being ( ( ) ( Relation-like REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) -valued Function-like V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V158() ) Point of ( ( ) ( non empty ) set ) ) st r : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) in the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) & q : ( ( ) ( Relation-like REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) -valued Function-like V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V158() ) Point of ( ( ) ( non empty ) set ) ) = f : ( ( Function-like V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) , the carrier of ((TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() V226() V227() ) L15()) | b₁ : ( ( non empty ) ( non empty ) Subset of ) ) : ( ( strict ) ( non empty strict TopSpace-like ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() V226() V227() ) L15()) ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of ((TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() V226() V227() ) L15()) | b₁ : ( ( non empty ) ( non empty ) Subset of ) ) : ( ( strict ) ( non empty strict TopSpace-like ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() V226() V227() ) L15()) ) : ( ( ) ( non empty ) set ) -valued Function-like total V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) , the carrier of ((TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() V226() V227() ) L15()) | b₁ : ( ( non empty ) ( non empty ) Subset of ) ) : ( ( strict ) ( non empty strict TopSpace-like ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() V226() V227() ) L15()) ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty V166() V167() V168() ) set ) , ( ( ) ( non empty ) set ) ) . r : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) holds
q : ( ( ) ( Relation-like REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) -valued Function-like V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V158() ) Point of ( ( ) ( non empty ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) = g : ( ( Function-like V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) , the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) ) ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) -valued Function-like total V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) , the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) ) ) Function of ( ( ) ( non empty V166() V167() V168() ) set ) , ( ( ) ( non empty V166() V167() V168() ) set ) ) . r : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: TOPREAL5:13

for P being ( ( non empty ) ( non empty ) Subset of )
for f being ( ( Function-like V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) , the carrier of ((TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() V226() V227() ) L15()) | b₁ : ( ( non empty ) ( non empty ) Subset of ) ) : ( ( strict ) ( non empty strict TopSpace-like ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() V226() V227() ) L15()) ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of ((TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() V226() V227() ) L15()) | b₁ : ( ( non empty ) ( non empty ) Subset of ) ) : ( ( strict ) ( non empty strict TopSpace-like ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() V226() V227() ) L15()) ) : ( ( ) ( non empty ) set ) -valued Function-like total V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) , the carrier of ((TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() V226() V227() ) L15()) | b₁ : ( ( non empty ) ( non empty ) Subset of ) ) : ( ( strict ) ( non empty strict TopSpace-like ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() V226() V227() ) L15()) ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty V166() V167() V168() ) set ) , ( ( ) ( non empty ) set ) ) st f : ( ( Function-like V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) , the carrier of ((TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() V226() V227() ) L15()) | b₁ : ( ( non empty ) ( non empty ) Subset of ) ) : ( ( strict ) ( non empty strict TopSpace-like ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() V226() V227() ) L15()) ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of ((TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() V226() V227() ) L15()) | b₁ : ( ( non empty ) ( non empty ) Subset of ) ) : ( ( strict ) ( non empty strict TopSpace-like ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() V226() V227() ) L15()) ) : ( ( ) ( non empty ) set ) -valued Function-like total V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) , the carrier of ((TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() V226() V227() ) L15()) | b₁ : ( ( non empty ) ( non empty ) Subset of ) ) : ( ( strict ) ( non empty strict TopSpace-like ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() V226() V227() ) L15()) ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty V166() V167() V168() ) set ) , ( ( ) ( non empty ) set ) ) is continuous holds
ex g being ( ( Function-like V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) , the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) ) ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) -valued Function-like total V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) , the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) ) ) Function of ( ( ) ( non empty V166() V167() V168() ) set ) , ( ( ) ( non empty V166() V167() V168() ) set ) ) st
( g : ( ( Function-like V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) , the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) ) ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) -valued Function-like total V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) , the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) ) ) Function of ( ( ) ( non empty V166() V167() V168() ) set ) , ( ( ) ( non empty V166() V167() V168() ) set ) ) is continuous & ( for r being ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) )
for q being ( ( ) ( Relation-like REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) -valued Function-like V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V158() ) Point of ( ( ) ( non empty ) set ) ) st r : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) in the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) & q : ( ( ) ( Relation-like REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) -valued Function-like V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V158() ) Point of ( ( ) ( non empty ) set ) ) = f : ( ( Function-like V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) , the carrier of ((TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() V226() V227() ) L15()) | b₁ : ( ( non empty ) ( non empty ) Subset of ) ) : ( ( strict ) ( non empty strict TopSpace-like ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() V226() V227() ) L15()) ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of ((TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() V226() V227() ) L15()) | b₁ : ( ( non empty ) ( non empty ) Subset of ) ) : ( ( strict ) ( non empty strict TopSpace-like ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() V226() V227() ) L15()) ) : ( ( ) ( non empty ) set ) -valued Function-like total V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) , the carrier of ((TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() V226() V227() ) L15()) | b₁ : ( ( non empty ) ( non empty ) Subset of ) ) : ( ( strict ) ( non empty strict TopSpace-like ) SubSpace of TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() V226() V227() ) L15()) ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty V166() V167() V168() ) set ) , ( ( ) ( non empty ) set ) ) . r : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) holds
q : ( ( ) ( Relation-like REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) -valued Function-like V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V158() ) Point of ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) = g : ( ( Function-like V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) , the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) ) ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) -valued Function-like total V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like V114() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) , the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V114() ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) ) ) Function of ( ( ) ( non empty V166() V167() V168() ) set ) , ( ( ) ( non empty V166() V167() V168() ) set ) ) . r : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: TOPREAL5:14

for P being ( ( non empty ) ( non empty ) Subset of ) st P : ( ( non empty ) ( non empty ) Subset of ) is being_simple_closed_curve holds
for r being ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) ex p being ( ( ) ( Relation-like REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) -valued Function-like V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V158() ) Point of ( ( ) ( non empty ) set ) ) st
( p : ( ( ) ( Relation-like REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) -valued Function-like V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V158() ) Point of ( ( ) ( non empty ) set ) ) in P : ( ( non empty ) ( non empty ) Subset of ) & not p : ( ( ) ( Relation-like REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) -valued Function-like V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V158() ) Point of ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) = r : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) ) ;

theorem :: TOPREAL5:15

for P being ( ( non empty ) ( non empty ) Subset of ) st P : ( ( non empty ) ( non empty ) Subset of ) is being_simple_closed_curve holds
for r being ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) ex p being ( ( ) ( Relation-like REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) -valued Function-like V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V158() ) Point of ( ( ) ( non empty ) set ) ) st
( p : ( ( ) ( Relation-like REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) -valued Function-like V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V158() ) Point of ( ( ) ( non empty ) set ) ) in P : ( ( non empty ) ( non empty ) Subset of ) & not p : ( ( ) ( Relation-like REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) -valued Function-like V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V158() ) Point of ( ( ) ( non empty ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) = r : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) ) ;

theorem :: TOPREAL5:16

for C being ( ( non empty compact ) ( non empty compact ) Subset of ) st C : ( ( non empty compact ) ( non empty compact ) Subset of ) is being_simple_closed_curve holds
N-bound C : ( ( non empty compact ) ( non empty compact ) Subset of ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) > S-bound C : ( ( non empty compact ) ( non empty compact ) Subset of ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) ;

theorem :: TOPREAL5:17

for C being ( ( non empty compact ) ( non empty compact ) Subset of ) st C : ( ( non empty compact ) ( non empty compact ) Subset of ) is being_simple_closed_curve holds
E-bound C : ( ( non empty compact ) ( non empty compact ) Subset of ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) > W-bound C : ( ( non empty compact ) ( non empty compact ) Subset of ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) ;

theorem :: TOPREAL5:18

for P being ( ( non empty compact ) ( non empty compact ) Subset of ) st P : ( ( non empty compact ) ( non empty compact ) Subset of ) is being_simple_closed_curve holds
S-min P : ( ( non empty compact ) ( non empty compact ) Subset of ) : ( ( ) ( Relation-like REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) -valued Function-like V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V158() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() V226() V227() ) L15()) : ( ( ) ( non empty ) set ) ) <> N-max P : ( ( non empty compact ) ( non empty compact ) Subset of ) : ( ( ) ( Relation-like REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) -valued Function-like V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V158() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() V226() V227() ) L15()) : ( ( ) ( non empty ) set ) ) ;

theorem :: TOPREAL5:19

for P being ( ( non empty compact ) ( non empty compact ) Subset of ) st P : ( ( non empty compact ) ( non empty compact ) Subset of ) is being_simple_closed_curve holds
W-min P : ( ( non empty compact ) ( non empty compact ) Subset of ) : ( ( ) ( Relation-like REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) -valued Function-like V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V158() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() V226() V227() ) L15()) : ( ( ) ( non empty ) set ) ) <> E-max P : ( ( non empty compact ) ( non empty compact ) Subset of ) : ( ( ) ( Relation-like REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) -valued Function-like V43(2 : ( ( ) ( non empty natural V11() real ext-real positive V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V158() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() V226() V227() ) L15()) : ( ( ) ( non empty ) set ) ) ;

registration

cluster being_simple_closed_curve -> being_simple_closed_curve non horizontal non vertical for ( ( ) ( ) Element of K6( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive V118() V119() V166() V167() V168() V169() V170() V171() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non empty V36() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() V226() V227() ) L15()) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ;

end;