:: RCOMP_3 semantic presentation

begin

registration
let X be ( ( non empty ) ( non empty ) set ) ;
cluster [#] X : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty non proper ) Element of K32(X : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) -> non empty ;
end;

registration
cluster -> real-membered for ( ( ) ( ) SubSpace of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning symmetric triangle Discerning real-membered ) MetrStruct ) ) ;
end;

theorem :: RCOMP_3:1
for X being ( ( non empty real-membered bounded_below ) ( non empty complex-membered ext-real-membered real-membered bounded_below ) set )
for Y being ( ( closed ) ( complex-membered ext-real-membered real-membered closed ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) st X : ( ( non empty real-membered bounded_below ) ( non empty complex-membered ext-real-membered real-membered bounded_below ) set ) c= Y : ( ( closed ) ( complex-membered ext-real-membered real-membered closed ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) holds
lower_bound X : ( ( non empty real-membered bounded_below ) ( non empty complex-membered ext-real-membered real-membered bounded_below ) set ) : ( ( real ) ( ext-real real V65() ) set ) in Y : ( ( closed ) ( complex-membered ext-real-membered real-membered closed ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) ;

theorem :: RCOMP_3:2
for X being ( ( non empty real-membered bounded_above ) ( non empty complex-membered ext-real-membered real-membered bounded_above ) set )
for Y being ( ( closed ) ( complex-membered ext-real-membered real-membered closed ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) st X : ( ( non empty real-membered bounded_above ) ( non empty complex-membered ext-real-membered real-membered bounded_above ) set ) c= Y : ( ( closed ) ( complex-membered ext-real-membered real-membered closed ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) holds
upper_bound X : ( ( non empty real-membered bounded_above ) ( non empty complex-membered ext-real-membered real-membered bounded_above ) set ) : ( ( real ) ( ext-real real V65() ) set ) in Y : ( ( closed ) ( complex-membered ext-real-membered real-membered closed ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) ;

theorem :: RCOMP_3:3
for X, Y being ( ( ) ( complex-membered ext-real-membered real-membered ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) holds Cl (X : ( ( ) ( complex-membered ext-real-membered real-membered ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) \/ Y : ( ( ) ( complex-membered ext-real-membered real-membered ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) ) : ( ( ) ( complex-membered ext-real-membered real-membered ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( complex-membered ext-real-membered real-membered closed ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) = (Cl X : ( ( ) ( complex-membered ext-real-membered real-membered ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) ) : ( ( ) ( complex-membered ext-real-membered real-membered closed ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) \/ (Cl Y : ( ( ) ( complex-membered ext-real-membered real-membered ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) ) : ( ( ) ( complex-membered ext-real-membered real-membered closed ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( complex-membered ext-real-membered real-membered ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ;

begin

registration
let r be ( ( real ) ( ext-real real V65() ) number ) ;
let s be ( ( ext-real ) ( ext-real ) number ) ;
cluster [.r : ( ( real ) ( ext-real real V65() ) set ) ,s : ( ( ext-real ) ( ext-real ) set ) .[ : ( ( ) ( complex-membered ext-real-membered real-membered non right_end interval ) set ) -> bounded_below ;
cluster ].s : ( ( ext-real ) ( ext-real ) set ) ,r : ( ( real ) ( ext-real real V65() ) set ) .] : ( ( ) ( complex-membered ext-real-membered real-membered non left_end interval ) set ) -> bounded_above ;
end;

registration
let r, s be ( ( real ) ( ext-real real V65() ) number ) ;
cluster [.r : ( ( real ) ( ext-real real V65() ) set ) ,s : ( ( real ) ( ext-real real V65() ) set ) .[ : ( ( ) ( complex-membered ext-real-membered real-membered non right_end bounded_below interval ) set ) -> real-bounded ;
cluster ].r : ( ( real ) ( ext-real real V65() ) set ) ,s : ( ( real ) ( ext-real real V65() ) set ) .] : ( ( ) ( complex-membered ext-real-membered real-membered non left_end bounded_above interval ) set ) -> real-bounded ;
cluster ].r : ( ( real ) ( ext-real real V65() ) set ) ,s : ( ( real ) ( ext-real real V65() ) set ) .[ : ( ( ) ( complex-membered ext-real-membered real-membered non left_end non right_end interval ) set ) -> real-bounded ;
end;

registration
cluster non empty complex-membered ext-real-membered real-membered open real-bounded interval for ( ( ) ( ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ;
end;

theorem :: RCOMP_3:4
for r, s being ( ( real ) ( ext-real real V65() ) number ) st r : ( ( real ) ( ext-real real V65() ) number ) < s : ( ( real ) ( ext-real real V65() ) number ) holds
lower_bound [.r : ( ( real ) ( ext-real real V65() ) number ) ,s : ( ( real ) ( ext-real real V65() ) number ) .[ : ( ( ) ( complex-membered ext-real-membered real-membered non right_end bounded_below bounded_above real-bounded interval ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( ext-real real V65() ) Element of REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) = r : ( ( real ) ( ext-real real V65() ) number ) ;

theorem :: RCOMP_3:5
for r, s being ( ( real ) ( ext-real real V65() ) number ) st r : ( ( real ) ( ext-real real V65() ) number ) < s : ( ( real ) ( ext-real real V65() ) number ) holds
upper_bound [.r : ( ( real ) ( ext-real real V65() ) number ) ,s : ( ( real ) ( ext-real real V65() ) number ) .[ : ( ( ) ( complex-membered ext-real-membered real-membered non right_end bounded_below bounded_above real-bounded interval ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( ext-real real V65() ) Element of REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) = s : ( ( real ) ( ext-real real V65() ) number ) ;

theorem :: RCOMP_3:6
for r, s being ( ( real ) ( ext-real real V65() ) number ) st r : ( ( real ) ( ext-real real V65() ) number ) < s : ( ( real ) ( ext-real real V65() ) number ) holds
lower_bound ].r : ( ( real ) ( ext-real real V65() ) number ) ,s : ( ( real ) ( ext-real real V65() ) number ) .] : ( ( ) ( complex-membered ext-real-membered real-membered non left_end bounded_below bounded_above real-bounded interval ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( ext-real real V65() ) Element of REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) = r : ( ( real ) ( ext-real real V65() ) number ) ;

theorem :: RCOMP_3:7
for r, s being ( ( real ) ( ext-real real V65() ) number ) st r : ( ( real ) ( ext-real real V65() ) number ) < s : ( ( real ) ( ext-real real V65() ) number ) holds
upper_bound ].r : ( ( real ) ( ext-real real V65() ) number ) ,s : ( ( real ) ( ext-real real V65() ) number ) .] : ( ( ) ( complex-membered ext-real-membered real-membered non left_end bounded_below bounded_above real-bounded interval ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( ext-real real V65() ) Element of REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) = s : ( ( real ) ( ext-real real V65() ) number ) ;

begin

theorem :: RCOMP_3:8
for a, b being ( ( real ) ( ext-real real V65() ) number ) st a : ( ( real ) ( ext-real real V65() ) number ) <= b : ( ( real ) ( ext-real real V65() ) number ) holds
[.a : ( ( real ) ( ext-real real V65() ) number ) ,b : ( ( real ) ( ext-real real V65() ) number ) .] : ( ( ) ( complex-membered ext-real-membered real-membered closed bounded_below bounded_above real-bounded interval ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) /\ ((left_closed_halfline a : ( ( real ) ( ext-real real V65() ) number ) ) : ( ( ) ( complex-membered ext-real-membered real-membered closed ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) \/ (right_closed_halfline b : ( ( real ) ( ext-real real V65() ) number ) ) : ( ( ) ( complex-membered ext-real-membered real-membered closed ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) : ( ( ) ( complex-membered ext-real-membered real-membered ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( complex-membered ext-real-membered real-membered ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) = {a : ( ( real ) ( ext-real real V65() ) number ) ,b : ( ( real ) ( ext-real real V65() ) number ) } : ( ( ) ( non empty finite complex-membered ext-real-membered real-membered left_end right_end bounded_below bounded_above real-bounded ) set ) ;

registration
let a be ( ( real ) ( ext-real real V65() ) number ) ;
cluster left_closed_halfline a : ( ( real ) ( ext-real real V65() ) set ) : ( ( ) ( complex-membered ext-real-membered real-membered closed ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -> non bounded_below bounded_above interval ;
cluster left_open_halfline a : ( ( real ) ( ext-real real V65() ) set ) : ( ( ) ( complex-membered ext-real-membered real-membered open ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -> non bounded_below bounded_above interval ;
cluster right_closed_halfline a : ( ( real ) ( ext-real real V65() ) set ) : ( ( ) ( complex-membered ext-real-membered real-membered closed ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -> bounded_below non bounded_above interval ;
cluster right_open_halfline a : ( ( real ) ( ext-real real V65() ) set ) : ( ( ) ( complex-membered ext-real-membered real-membered open ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -> bounded_below non bounded_above interval ;
end;

theorem :: RCOMP_3:9
for a being ( ( real ) ( ext-real real V65() ) number ) holds upper_bound (left_closed_halfline a : ( ( real ) ( ext-real real V65() ) number ) ) : ( ( ) ( complex-membered ext-real-membered real-membered closed non bounded_below bounded_above interval ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( ext-real real V65() ) Element of REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) = a : ( ( real ) ( ext-real real V65() ) number ) ;

theorem :: RCOMP_3:10
for a being ( ( real ) ( ext-real real V65() ) number ) holds upper_bound (left_open_halfline a : ( ( real ) ( ext-real real V65() ) number ) ) : ( ( ) ( complex-membered ext-real-membered real-membered open non bounded_below bounded_above interval ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( ext-real real V65() ) Element of REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) = a : ( ( real ) ( ext-real real V65() ) number ) ;

theorem :: RCOMP_3:11
for a being ( ( real ) ( ext-real real V65() ) number ) holds lower_bound (right_closed_halfline a : ( ( real ) ( ext-real real V65() ) number ) ) : ( ( ) ( complex-membered ext-real-membered real-membered closed bounded_below non bounded_above interval ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( ext-real real V65() ) Element of REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) = a : ( ( real ) ( ext-real real V65() ) number ) ;

theorem :: RCOMP_3:12
for a being ( ( real ) ( ext-real real V65() ) number ) holds lower_bound (right_open_halfline a : ( ( real ) ( ext-real real V65() ) number ) ) : ( ( ) ( complex-membered ext-real-membered real-membered open bounded_below non bounded_above interval ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( ext-real real V65() ) Element of REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) = a : ( ( real ) ( ext-real real V65() ) number ) ;

begin

registration
cluster [#] REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non proper complex-membered ext-real-membered real-membered closed open ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -> non bounded_below non bounded_above interval ;
end;

theorem :: RCOMP_3:13
for X being ( ( real-bounded interval ) ( complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) st lower_bound X : ( ( real-bounded interval ) ( complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( ext-real real V65() ) Element of REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) in X : ( ( real-bounded interval ) ( complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) & upper_bound X : ( ( real-bounded interval ) ( complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( ext-real real V65() ) Element of REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) in X : ( ( real-bounded interval ) ( complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) holds
X : ( ( real-bounded interval ) ( complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) = [.(lower_bound X : ( ( real-bounded interval ) ( complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) ) : ( ( ) ( ext-real real V65() ) Element of REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) ,(upper_bound X : ( ( real-bounded interval ) ( complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) ) : ( ( ) ( ext-real real V65() ) Element of REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) .] : ( ( ) ( complex-membered ext-real-membered real-membered closed bounded_below bounded_above real-bounded interval ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ;

theorem :: RCOMP_3:14
for X being ( ( real-bounded ) ( complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) st not lower_bound X : ( ( real-bounded ) ( complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( ext-real real V65() ) Element of REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) in X : ( ( real-bounded ) ( complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) holds
X : ( ( real-bounded ) ( complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) c= ].(lower_bound X : ( ( real-bounded ) ( complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) ) : ( ( ) ( ext-real real V65() ) Element of REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) ,(upper_bound X : ( ( real-bounded ) ( complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) ) : ( ( ) ( ext-real real V65() ) Element of REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) .] : ( ( ) ( complex-membered ext-real-membered real-membered non left_end bounded_below bounded_above real-bounded interval ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ;

theorem :: RCOMP_3:15
for X being ( ( real-bounded interval ) ( complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) st not lower_bound X : ( ( real-bounded interval ) ( complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( ext-real real V65() ) Element of REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) in X : ( ( real-bounded interval ) ( complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) & upper_bound X : ( ( real-bounded interval ) ( complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( ext-real real V65() ) Element of REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) in X : ( ( real-bounded interval ) ( complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) holds
X : ( ( real-bounded interval ) ( complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) = ].(lower_bound X : ( ( real-bounded interval ) ( complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) ) : ( ( ) ( ext-real real V65() ) Element of REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) ,(upper_bound X : ( ( real-bounded interval ) ( complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) ) : ( ( ) ( ext-real real V65() ) Element of REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) .] : ( ( ) ( complex-membered ext-real-membered real-membered non left_end bounded_below bounded_above real-bounded interval ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ;

theorem :: RCOMP_3:16
for X being ( ( real-bounded ) ( complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) st not upper_bound X : ( ( real-bounded ) ( complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( ext-real real V65() ) Element of REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) in X : ( ( real-bounded ) ( complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) holds
X : ( ( real-bounded ) ( complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) c= [.(lower_bound X : ( ( real-bounded ) ( complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) ) : ( ( ) ( ext-real real V65() ) Element of REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) ,(upper_bound X : ( ( real-bounded ) ( complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) ) : ( ( ) ( ext-real real V65() ) Element of REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) .[ : ( ( ) ( complex-membered ext-real-membered real-membered non right_end bounded_below bounded_above real-bounded interval ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ;

theorem :: RCOMP_3:17
for X being ( ( real-bounded interval ) ( complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) st lower_bound X : ( ( real-bounded interval ) ( complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( ext-real real V65() ) Element of REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) in X : ( ( real-bounded interval ) ( complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) & not upper_bound X : ( ( real-bounded interval ) ( complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( ext-real real V65() ) Element of REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) in X : ( ( real-bounded interval ) ( complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) holds
X : ( ( real-bounded interval ) ( complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) = [.(lower_bound X : ( ( real-bounded interval ) ( complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) ) : ( ( ) ( ext-real real V65() ) Element of REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) ,(upper_bound X : ( ( real-bounded interval ) ( complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) ) : ( ( ) ( ext-real real V65() ) Element of REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) .[ : ( ( ) ( complex-membered ext-real-membered real-membered non right_end bounded_below bounded_above real-bounded interval ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ;

theorem :: RCOMP_3:18
for X being ( ( real-bounded ) ( complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) st not lower_bound X : ( ( real-bounded ) ( complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( ext-real real V65() ) Element of REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) in X : ( ( real-bounded ) ( complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) & not upper_bound X : ( ( real-bounded ) ( complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( ext-real real V65() ) Element of REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) in X : ( ( real-bounded ) ( complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) holds
X : ( ( real-bounded ) ( complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) c= ].(lower_bound X : ( ( real-bounded ) ( complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) ) : ( ( ) ( ext-real real V65() ) Element of REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) ,(upper_bound X : ( ( real-bounded ) ( complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) ) : ( ( ) ( ext-real real V65() ) Element of REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) .[ : ( ( ) ( complex-membered ext-real-membered real-membered open non left_end non right_end bounded_below bounded_above real-bounded interval ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ;

theorem :: RCOMP_3:19
for X being ( ( non empty real-bounded interval ) ( non empty complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) st not lower_bound X : ( ( non empty real-bounded interval ) ( non empty complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( ext-real real V65() ) Element of REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) in X : ( ( non empty real-bounded interval ) ( non empty complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) & not upper_bound X : ( ( non empty real-bounded interval ) ( non empty complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( ext-real real V65() ) Element of REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) in X : ( ( non empty real-bounded interval ) ( non empty complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) holds
X : ( ( non empty real-bounded interval ) ( non empty complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) = ].(lower_bound X : ( ( non empty real-bounded interval ) ( non empty complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) ) : ( ( ) ( ext-real real V65() ) Element of REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) ,(upper_bound X : ( ( non empty real-bounded interval ) ( non empty complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) ) : ( ( ) ( ext-real real V65() ) Element of REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) .[ : ( ( ) ( complex-membered ext-real-membered real-membered open non left_end non right_end bounded_below bounded_above real-bounded interval ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ;

theorem :: RCOMP_3:20
for X being ( ( ) ( complex-membered ext-real-membered real-membered ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) st X : ( ( ) ( complex-membered ext-real-membered real-membered ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) is bounded_above holds
X : ( ( ) ( complex-membered ext-real-membered real-membered ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) c= left_closed_halfline (upper_bound X : ( ( ) ( complex-membered ext-real-membered real-membered ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) ) : ( ( ) ( ext-real real V65() ) Element of REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( complex-membered ext-real-membered real-membered closed non bounded_below bounded_above interval ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ;

theorem :: RCOMP_3:21
for X being ( ( interval ) ( complex-membered ext-real-membered real-membered interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) st not X : ( ( interval ) ( complex-membered ext-real-membered real-membered interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) is bounded_below & X : ( ( interval ) ( complex-membered ext-real-membered real-membered interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) is bounded_above & upper_bound X : ( ( interval ) ( complex-membered ext-real-membered real-membered interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( ext-real real V65() ) Element of REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) in X : ( ( interval ) ( complex-membered ext-real-membered real-membered interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) holds
X : ( ( interval ) ( complex-membered ext-real-membered real-membered interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) = left_closed_halfline (upper_bound X : ( ( interval ) ( complex-membered ext-real-membered real-membered interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) ) : ( ( ) ( ext-real real V65() ) Element of REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( complex-membered ext-real-membered real-membered closed non bounded_below bounded_above interval ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ;

theorem :: RCOMP_3:22
for X being ( ( ) ( complex-membered ext-real-membered real-membered ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) st X : ( ( ) ( complex-membered ext-real-membered real-membered ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) is bounded_above & not upper_bound X : ( ( ) ( complex-membered ext-real-membered real-membered ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( ext-real real V65() ) Element of REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) in X : ( ( ) ( complex-membered ext-real-membered real-membered ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) holds
X : ( ( ) ( complex-membered ext-real-membered real-membered ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) c= left_open_halfline (upper_bound X : ( ( ) ( complex-membered ext-real-membered real-membered ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) ) : ( ( ) ( ext-real real V65() ) Element of REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( complex-membered ext-real-membered real-membered open non bounded_below bounded_above interval ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ;

theorem :: RCOMP_3:23
for X being ( ( non empty interval ) ( non empty complex-membered ext-real-membered real-membered interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) st not X : ( ( non empty interval ) ( non empty complex-membered ext-real-membered real-membered interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) is bounded_below & X : ( ( non empty interval ) ( non empty complex-membered ext-real-membered real-membered interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) is bounded_above & not upper_bound X : ( ( non empty interval ) ( non empty complex-membered ext-real-membered real-membered interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( ext-real real V65() ) Element of REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) in X : ( ( non empty interval ) ( non empty complex-membered ext-real-membered real-membered interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) holds
X : ( ( non empty interval ) ( non empty complex-membered ext-real-membered real-membered interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) = left_open_halfline (upper_bound X : ( ( non empty interval ) ( non empty complex-membered ext-real-membered real-membered interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) ) : ( ( ) ( ext-real real V65() ) Element of REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( complex-membered ext-real-membered real-membered open non bounded_below bounded_above interval ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ;

theorem :: RCOMP_3:24
for X being ( ( ) ( complex-membered ext-real-membered real-membered ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) st X : ( ( ) ( complex-membered ext-real-membered real-membered ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) is bounded_below holds
X : ( ( ) ( complex-membered ext-real-membered real-membered ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) c= right_closed_halfline (lower_bound X : ( ( ) ( complex-membered ext-real-membered real-membered ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) ) : ( ( ) ( ext-real real V65() ) Element of REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( complex-membered ext-real-membered real-membered closed bounded_below non bounded_above interval ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ;

theorem :: RCOMP_3:25
for X being ( ( interval ) ( complex-membered ext-real-membered real-membered interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) st X : ( ( interval ) ( complex-membered ext-real-membered real-membered interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) is bounded_below & not X : ( ( interval ) ( complex-membered ext-real-membered real-membered interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) is bounded_above & lower_bound X : ( ( interval ) ( complex-membered ext-real-membered real-membered interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( ext-real real V65() ) Element of REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) in X : ( ( interval ) ( complex-membered ext-real-membered real-membered interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) holds
X : ( ( interval ) ( complex-membered ext-real-membered real-membered interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) = right_closed_halfline (lower_bound X : ( ( interval ) ( complex-membered ext-real-membered real-membered interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) ) : ( ( ) ( ext-real real V65() ) Element of REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( complex-membered ext-real-membered real-membered closed bounded_below non bounded_above interval ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ;

theorem :: RCOMP_3:26
for X being ( ( ) ( complex-membered ext-real-membered real-membered ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) st X : ( ( ) ( complex-membered ext-real-membered real-membered ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) is bounded_below & not lower_bound X : ( ( ) ( complex-membered ext-real-membered real-membered ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( ext-real real V65() ) Element of REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) in X : ( ( ) ( complex-membered ext-real-membered real-membered ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) holds
X : ( ( ) ( complex-membered ext-real-membered real-membered ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) c= right_open_halfline (lower_bound X : ( ( ) ( complex-membered ext-real-membered real-membered ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) ) : ( ( ) ( ext-real real V65() ) Element of REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( complex-membered ext-real-membered real-membered open bounded_below non bounded_above interval ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ;

theorem :: RCOMP_3:27
for X being ( ( non empty interval ) ( non empty complex-membered ext-real-membered real-membered interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) st X : ( ( non empty interval ) ( non empty complex-membered ext-real-membered real-membered interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) is bounded_below & not X : ( ( non empty interval ) ( non empty complex-membered ext-real-membered real-membered interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) is bounded_above & not lower_bound X : ( ( non empty interval ) ( non empty complex-membered ext-real-membered real-membered interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( ext-real real V65() ) Element of REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) in X : ( ( non empty interval ) ( non empty complex-membered ext-real-membered real-membered interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) holds
X : ( ( non empty interval ) ( non empty complex-membered ext-real-membered real-membered interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) = right_open_halfline (lower_bound X : ( ( non empty interval ) ( non empty complex-membered ext-real-membered real-membered interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) ) : ( ( ) ( ext-real real V65() ) Element of REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( complex-membered ext-real-membered real-membered open bounded_below non bounded_above interval ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ;

theorem :: RCOMP_3:28
for X being ( ( interval ) ( complex-membered ext-real-membered real-membered interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) st not X : ( ( interval ) ( complex-membered ext-real-membered real-membered interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) is bounded_above & not X : ( ( interval ) ( complex-membered ext-real-membered real-membered interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) is bounded_below holds
X : ( ( interval ) ( complex-membered ext-real-membered real-membered interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) = REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ;

theorem :: RCOMP_3:29
for X being ( ( interval ) ( complex-membered ext-real-membered real-membered interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) holds
( X : ( ( interval ) ( complex-membered ext-real-membered real-membered interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) is empty or X : ( ( interval ) ( complex-membered ext-real-membered real-membered interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) = REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) or ex a being ( ( real ) ( ext-real real V65() ) number ) st X : ( ( interval ) ( complex-membered ext-real-membered real-membered interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) = left_closed_halfline a : ( ( real ) ( ext-real real V65() ) number ) : ( ( ) ( complex-membered ext-real-membered real-membered closed non bounded_below bounded_above interval ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) or ex a being ( ( real ) ( ext-real real V65() ) number ) st X : ( ( interval ) ( complex-membered ext-real-membered real-membered interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) = left_open_halfline a : ( ( real ) ( ext-real real V65() ) number ) : ( ( ) ( complex-membered ext-real-membered real-membered open non bounded_below bounded_above interval ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) or ex a being ( ( real ) ( ext-real real V65() ) number ) st X : ( ( interval ) ( complex-membered ext-real-membered real-membered interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) = right_closed_halfline a : ( ( real ) ( ext-real real V65() ) number ) : ( ( ) ( complex-membered ext-real-membered real-membered closed bounded_below non bounded_above interval ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) or ex a being ( ( real ) ( ext-real real V65() ) number ) st X : ( ( interval ) ( complex-membered ext-real-membered real-membered interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) = right_open_halfline a : ( ( real ) ( ext-real real V65() ) number ) : ( ( ) ( complex-membered ext-real-membered real-membered open bounded_below non bounded_above interval ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) or ex a, b being ( ( real ) ( ext-real real V65() ) number ) st
( a : ( ( real ) ( ext-real real V65() ) number ) <= b : ( ( real ) ( ext-real real V65() ) number ) & X : ( ( interval ) ( complex-membered ext-real-membered real-membered interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) = [.a : ( ( real ) ( ext-real real V65() ) number ) ,b : ( ( real ) ( ext-real real V65() ) number ) .] : ( ( ) ( complex-membered ext-real-membered real-membered closed bounded_below bounded_above real-bounded interval ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) or ex a, b being ( ( real ) ( ext-real real V65() ) number ) st
( a : ( ( real ) ( ext-real real V65() ) number ) < b : ( ( real ) ( ext-real real V65() ) number ) & X : ( ( interval ) ( complex-membered ext-real-membered real-membered interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) = [.a : ( ( real ) ( ext-real real V65() ) number ) ,b : ( ( real ) ( ext-real real V65() ) number ) .[ : ( ( ) ( complex-membered ext-real-membered real-membered non right_end bounded_below bounded_above real-bounded interval ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) or ex a, b being ( ( real ) ( ext-real real V65() ) number ) st
( a : ( ( real ) ( ext-real real V65() ) number ) < b : ( ( real ) ( ext-real real V65() ) number ) & X : ( ( interval ) ( complex-membered ext-real-membered real-membered interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) = ].a : ( ( real ) ( ext-real real V65() ) number ) ,b : ( ( real ) ( ext-real real V65() ) number ) .] : ( ( ) ( complex-membered ext-real-membered real-membered non left_end bounded_below bounded_above real-bounded interval ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) or ex a, b being ( ( real ) ( ext-real real V65() ) number ) st
( a : ( ( real ) ( ext-real real V65() ) number ) < b : ( ( real ) ( ext-real real V65() ) number ) & X : ( ( interval ) ( complex-membered ext-real-membered real-membered interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) = ].a : ( ( real ) ( ext-real real V65() ) number ) ,b : ( ( real ) ( ext-real real V65() ) number ) .[ : ( ( ) ( complex-membered ext-real-membered real-membered open non left_end non right_end bounded_below bounded_above real-bounded interval ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) ) ;

theorem :: RCOMP_3:30
for r being ( ( real ) ( ext-real real V65() ) number )
for X being ( ( non empty interval ) ( non empty complex-membered ext-real-membered real-membered interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) holds
( r : ( ( real ) ( ext-real real V65() ) number ) in X : ( ( non empty interval ) ( non empty complex-membered ext-real-membered real-membered interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) or r : ( ( real ) ( ext-real real V65() ) number ) <= lower_bound X : ( ( non empty interval ) ( non empty complex-membered ext-real-membered real-membered interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( ext-real real V65() ) Element of REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) or upper_bound X : ( ( non empty interval ) ( non empty complex-membered ext-real-membered real-membered interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( ext-real real V65() ) Element of REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) <= r : ( ( real ) ( ext-real real V65() ) number ) ) ;

theorem :: RCOMP_3:31
for X, Y being ( ( non empty real-bounded interval ) ( non empty complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) st lower_bound X : ( ( non empty real-bounded interval ) ( non empty complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( ext-real real V65() ) Element of REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) <= lower_bound Y : ( ( non empty real-bounded interval ) ( non empty complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( ext-real real V65() ) Element of REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) & upper_bound Y : ( ( non empty real-bounded interval ) ( non empty complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( ext-real real V65() ) Element of REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) <= upper_bound X : ( ( non empty real-bounded interval ) ( non empty complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( ext-real real V65() ) Element of REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) & ( lower_bound X : ( ( non empty real-bounded interval ) ( non empty complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( ext-real real V65() ) Element of REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) = lower_bound Y : ( ( non empty real-bounded interval ) ( non empty complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( ext-real real V65() ) Element of REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) & lower_bound Y : ( ( non empty real-bounded interval ) ( non empty complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( ext-real real V65() ) Element of REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) in Y : ( ( non empty real-bounded interval ) ( non empty complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) implies lower_bound X : ( ( non empty real-bounded interval ) ( non empty complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( ext-real real V65() ) Element of REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) in X : ( ( non empty real-bounded interval ) ( non empty complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) ) & ( upper_bound X : ( ( non empty real-bounded interval ) ( non empty complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( ext-real real V65() ) Element of REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) = upper_bound Y : ( ( non empty real-bounded interval ) ( non empty complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( ext-real real V65() ) Element of REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) & upper_bound Y : ( ( non empty real-bounded interval ) ( non empty complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( ext-real real V65() ) Element of REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) in Y : ( ( non empty real-bounded interval ) ( non empty complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) implies upper_bound X : ( ( non empty real-bounded interval ) ( non empty complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( ext-real real V65() ) Element of REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) in X : ( ( non empty real-bounded interval ) ( non empty complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) ) holds
Y : ( ( non empty real-bounded interval ) ( non empty complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) c= X : ( ( non empty real-bounded interval ) ( non empty complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) ;

registration
cluster non empty complex-membered ext-real-membered real-membered closed open non real-bounded interval for ( ( ) ( ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ;
end;

begin

theorem :: RCOMP_3:32
for a, b being ( ( real ) ( ext-real real V65() ) number )
for X being ( ( ) ( complex-membered ext-real-membered real-membered ) Subset of ) st a : ( ( real ) ( ext-real real V65() ) number ) <= b : ( ( real ) ( ext-real real V65() ) number ) & X : ( ( ) ( complex-membered ext-real-membered real-membered ) Subset of ) = [.a : ( ( real ) ( ext-real real V65() ) number ) ,b : ( ( real ) ( ext-real real V65() ) number ) .] : ( ( ) ( complex-membered ext-real-membered real-membered closed bounded_below bounded_above real-bounded interval ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) holds
Fr X : ( ( ) ( complex-membered ext-real-membered real-membered ) Subset of ) : ( ( ) ( closed complex-membered ext-real-membered real-membered ) Element of K32( the carrier of R^1 : ( ( interval ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected real-membered interval V241() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 T_2 real-membered ) TopStruct ) ) : ( ( ) ( non empty complex-membered ext-real-membered real-membered ) set ) ) : ( ( ) ( non empty ) set ) ) = {a : ( ( real ) ( ext-real real V65() ) number ) ,b : ( ( real ) ( ext-real real V65() ) number ) } : ( ( ) ( non empty finite complex-membered ext-real-membered real-membered left_end right_end bounded_below bounded_above real-bounded ) set ) ;

theorem :: RCOMP_3:33
for a, b being ( ( real ) ( ext-real real V65() ) number )
for X being ( ( ) ( complex-membered ext-real-membered real-membered ) Subset of ) st a : ( ( real ) ( ext-real real V65() ) number ) < b : ( ( real ) ( ext-real real V65() ) number ) & X : ( ( ) ( complex-membered ext-real-membered real-membered ) Subset of ) = ].a : ( ( real ) ( ext-real real V65() ) number ) ,b : ( ( real ) ( ext-real real V65() ) number ) .[ : ( ( ) ( complex-membered ext-real-membered real-membered open non left_end non right_end bounded_below bounded_above real-bounded interval ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) holds
Fr X : ( ( ) ( complex-membered ext-real-membered real-membered ) Subset of ) : ( ( ) ( closed complex-membered ext-real-membered real-membered ) Element of K32( the carrier of R^1 : ( ( interval ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected real-membered interval V241() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 T_2 real-membered ) TopStruct ) ) : ( ( ) ( non empty complex-membered ext-real-membered real-membered ) set ) ) : ( ( ) ( non empty ) set ) ) = {a : ( ( real ) ( ext-real real V65() ) number ) ,b : ( ( real ) ( ext-real real V65() ) number ) } : ( ( ) ( non empty finite complex-membered ext-real-membered real-membered left_end right_end bounded_below bounded_above real-bounded ) set ) ;

theorem :: RCOMP_3:34
for a, b being ( ( real ) ( ext-real real V65() ) number )
for X being ( ( ) ( complex-membered ext-real-membered real-membered ) Subset of ) st a : ( ( real ) ( ext-real real V65() ) number ) < b : ( ( real ) ( ext-real real V65() ) number ) & X : ( ( ) ( complex-membered ext-real-membered real-membered ) Subset of ) = [.a : ( ( real ) ( ext-real real V65() ) number ) ,b : ( ( real ) ( ext-real real V65() ) number ) .[ : ( ( ) ( complex-membered ext-real-membered real-membered non right_end bounded_below bounded_above real-bounded interval ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) holds
Fr X : ( ( ) ( complex-membered ext-real-membered real-membered ) Subset of ) : ( ( ) ( closed complex-membered ext-real-membered real-membered ) Element of K32( the carrier of R^1 : ( ( interval ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected real-membered interval V241() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 T_2 real-membered ) TopStruct ) ) : ( ( ) ( non empty complex-membered ext-real-membered real-membered ) set ) ) : ( ( ) ( non empty ) set ) ) = {a : ( ( real ) ( ext-real real V65() ) number ) ,b : ( ( real ) ( ext-real real V65() ) number ) } : ( ( ) ( non empty finite complex-membered ext-real-membered real-membered left_end right_end bounded_below bounded_above real-bounded ) set ) ;

theorem :: RCOMP_3:35
for a, b being ( ( real ) ( ext-real real V65() ) number )
for X being ( ( ) ( complex-membered ext-real-membered real-membered ) Subset of ) st a : ( ( real ) ( ext-real real V65() ) number ) < b : ( ( real ) ( ext-real real V65() ) number ) & X : ( ( ) ( complex-membered ext-real-membered real-membered ) Subset of ) = ].a : ( ( real ) ( ext-real real V65() ) number ) ,b : ( ( real ) ( ext-real real V65() ) number ) .] : ( ( ) ( complex-membered ext-real-membered real-membered non left_end bounded_below bounded_above real-bounded interval ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) holds
Fr X : ( ( ) ( complex-membered ext-real-membered real-membered ) Subset of ) : ( ( ) ( closed complex-membered ext-real-membered real-membered ) Element of K32( the carrier of R^1 : ( ( interval ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected real-membered interval V241() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 T_2 real-membered ) TopStruct ) ) : ( ( ) ( non empty complex-membered ext-real-membered real-membered ) set ) ) : ( ( ) ( non empty ) set ) ) = {a : ( ( real ) ( ext-real real V65() ) number ) ,b : ( ( real ) ( ext-real real V65() ) number ) } : ( ( ) ( non empty finite complex-membered ext-real-membered real-membered left_end right_end bounded_below bounded_above real-bounded ) set ) ;

theorem :: RCOMP_3:36
for a, b being ( ( real ) ( ext-real real V65() ) number )
for X being ( ( ) ( complex-membered ext-real-membered real-membered ) Subset of ) st X : ( ( ) ( complex-membered ext-real-membered real-membered ) Subset of ) = [.a : ( ( real ) ( ext-real real V65() ) number ) ,b : ( ( real ) ( ext-real real V65() ) number ) .] : ( ( ) ( complex-membered ext-real-membered real-membered closed bounded_below bounded_above real-bounded interval ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) holds
Int X : ( ( ) ( complex-membered ext-real-membered real-membered ) Subset of ) : ( ( ) ( open complex-membered ext-real-membered real-membered ) Element of K32( the carrier of R^1 : ( ( interval ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected real-membered interval V241() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 T_2 real-membered ) TopStruct ) ) : ( ( ) ( non empty complex-membered ext-real-membered real-membered ) set ) ) : ( ( ) ( non empty ) set ) ) = ].a : ( ( real ) ( ext-real real V65() ) number ) ,b : ( ( real ) ( ext-real real V65() ) number ) .[ : ( ( ) ( complex-membered ext-real-membered real-membered open non left_end non right_end bounded_below bounded_above real-bounded interval ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ;

theorem :: RCOMP_3:37
for a, b being ( ( real ) ( ext-real real V65() ) number )
for X being ( ( ) ( complex-membered ext-real-membered real-membered ) Subset of ) st X : ( ( ) ( complex-membered ext-real-membered real-membered ) Subset of ) = ].a : ( ( real ) ( ext-real real V65() ) number ) ,b : ( ( real ) ( ext-real real V65() ) number ) .[ : ( ( ) ( complex-membered ext-real-membered real-membered open non left_end non right_end bounded_below bounded_above real-bounded interval ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) holds
Int X : ( ( ) ( complex-membered ext-real-membered real-membered ) Subset of ) : ( ( ) ( open complex-membered ext-real-membered real-membered ) Element of K32( the carrier of R^1 : ( ( interval ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected real-membered interval V241() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 T_2 real-membered ) TopStruct ) ) : ( ( ) ( non empty complex-membered ext-real-membered real-membered ) set ) ) : ( ( ) ( non empty ) set ) ) = ].a : ( ( real ) ( ext-real real V65() ) number ) ,b : ( ( real ) ( ext-real real V65() ) number ) .[ : ( ( ) ( complex-membered ext-real-membered real-membered open non left_end non right_end bounded_below bounded_above real-bounded interval ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ;

theorem :: RCOMP_3:38
for a, b being ( ( real ) ( ext-real real V65() ) number )
for X being ( ( ) ( complex-membered ext-real-membered real-membered ) Subset of ) st X : ( ( ) ( complex-membered ext-real-membered real-membered ) Subset of ) = [.a : ( ( real ) ( ext-real real V65() ) number ) ,b : ( ( real ) ( ext-real real V65() ) number ) .[ : ( ( ) ( complex-membered ext-real-membered real-membered non right_end bounded_below bounded_above real-bounded interval ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) holds
Int X : ( ( ) ( complex-membered ext-real-membered real-membered ) Subset of ) : ( ( ) ( open complex-membered ext-real-membered real-membered ) Element of K32( the carrier of R^1 : ( ( interval ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected real-membered interval V241() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 T_2 real-membered ) TopStruct ) ) : ( ( ) ( non empty complex-membered ext-real-membered real-membered ) set ) ) : ( ( ) ( non empty ) set ) ) = ].a : ( ( real ) ( ext-real real V65() ) number ) ,b : ( ( real ) ( ext-real real V65() ) number ) .[ : ( ( ) ( complex-membered ext-real-membered real-membered open non left_end non right_end bounded_below bounded_above real-bounded interval ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ;

theorem :: RCOMP_3:39
for a, b being ( ( real ) ( ext-real real V65() ) number )
for X being ( ( ) ( complex-membered ext-real-membered real-membered ) Subset of ) st X : ( ( ) ( complex-membered ext-real-membered real-membered ) Subset of ) = ].a : ( ( real ) ( ext-real real V65() ) number ) ,b : ( ( real ) ( ext-real real V65() ) number ) .] : ( ( ) ( complex-membered ext-real-membered real-membered non left_end bounded_below bounded_above real-bounded interval ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) holds
Int X : ( ( ) ( complex-membered ext-real-membered real-membered ) Subset of ) : ( ( ) ( open complex-membered ext-real-membered real-membered ) Element of K32( the carrier of R^1 : ( ( interval ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected real-membered interval V241() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 T_2 real-membered ) TopStruct ) ) : ( ( ) ( non empty complex-membered ext-real-membered real-membered ) set ) ) : ( ( ) ( non empty ) set ) ) = ].a : ( ( real ) ( ext-real real V65() ) number ) ,b : ( ( real ) ( ext-real real V65() ) number ) .[ : ( ( ) ( complex-membered ext-real-membered real-membered open non left_end non right_end bounded_below bounded_above real-bounded interval ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ;

registration
let T be ( ( real-membered ) ( real-membered ) TopStruct ) ;
let X be ( ( interval ) ( complex-membered ext-real-membered real-membered interval ) Subset of ) ;
cluster T : ( ( real-membered ) ( real-membered ) TopStruct ) | X : ( ( interval ) ( complex-membered ext-real-membered real-membered interval ) Element of K32( the carrier of T : ( ( real-membered ) ( real-membered ) TopStruct ) : ( ( ) ( complex-membered ext-real-membered real-membered ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( strict real-membered ) SubSpace of T : ( ( real-membered ) ( real-membered ) TopStruct ) ) -> strict interval ;
end;

registration
let A be ( ( interval ) ( complex-membered ext-real-membered real-membered interval ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) ;
cluster R^1 A : ( ( interval ) ( complex-membered ext-real-membered real-membered interval ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( complex-membered ext-real-membered real-membered ) Element of K32( the carrier of R^1 : ( ( interval ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected real-membered interval V241() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 T_2 real-membered ) TopStruct ) ) : ( ( ) ( non empty complex-membered ext-real-membered real-membered ) set ) ) : ( ( ) ( non empty ) set ) ) -> interval ;
end;

registration
cluster connected -> interval for ( ( ) ( ) Element of K32( the carrier of R^1 : ( ( interval ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected real-membered interval V241() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 T_2 real-membered ) TopStruct ) ) : ( ( ) ( non empty complex-membered ext-real-membered real-membered ) set ) ) : ( ( ) ( non empty ) set ) ) ;
cluster interval -> connected for ( ( ) ( ) Element of K32( the carrier of R^1 : ( ( interval ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected real-membered interval V241() ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 T_2 real-membered ) TopStruct ) ) : ( ( ) ( non empty complex-membered ext-real-membered real-membered ) set ) ) : ( ( ) ( non empty ) set ) ) ;
end;

begin

registration
let r be ( ( real ) ( ext-real real V65() ) number ) ;
cluster Closed-Interval-TSpace (r : ( ( real ) ( ext-real real V65() ) set ) ,r : ( ( real ) ( ext-real real V65() ) set ) ) : ( ( non empty strict ) ( non empty strict TopSpace-like real-membered ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 T_2 real-membered ) TopStruct ) ) -> non empty 1 : ( ( ) ( ordinal natural non empty ext-real positive non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) -element strict ;
end;

theorem :: RCOMP_3:40
for r, s being ( ( real ) ( ext-real real V65() ) number ) st r : ( ( real ) ( ext-real real V65() ) number ) <= s : ( ( real ) ( ext-real real V65() ) number ) holds
for A being ( ( ) ( complex-membered ext-real-membered real-membered ) Subset of ) holds A : ( ( ) ( complex-membered ext-real-membered real-membered ) Subset of ) is ( ( real-bounded ) ( complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) ;

theorem :: RCOMP_3:41
for r, s, a, b being ( ( real ) ( ext-real real V65() ) number ) st r : ( ( real ) ( ext-real real V65() ) number ) <= s : ( ( real ) ( ext-real real V65() ) number ) holds
for X being ( ( ) ( complex-membered ext-real-membered real-membered ) Subset of ) st X : ( ( ) ( complex-membered ext-real-membered real-membered ) Subset of ) = [.a : ( ( real ) ( ext-real real V65() ) number ) ,b : ( ( real ) ( ext-real real V65() ) number ) .[ : ( ( ) ( complex-membered ext-real-membered real-membered non right_end bounded_below bounded_above real-bounded interval ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) & r : ( ( real ) ( ext-real real V65() ) number ) < a : ( ( real ) ( ext-real real V65() ) number ) & b : ( ( real ) ( ext-real real V65() ) number ) <= s : ( ( real ) ( ext-real real V65() ) number ) holds
Int X : ( ( ) ( complex-membered ext-real-membered real-membered ) Subset of ) : ( ( ) ( open complex-membered ext-real-membered real-membered ) Element of K32( the carrier of (Closed-Interval-TSpace (b1 : ( ( real ) ( ext-real real V65() ) number ) ,b2 : ( ( real ) ( ext-real real V65() ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like real-membered ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 T_2 real-membered ) TopStruct ) ) : ( ( ) ( non empty complex-membered ext-real-membered real-membered ) set ) ) : ( ( ) ( non empty ) set ) ) = ].a : ( ( real ) ( ext-real real V65() ) number ) ,b : ( ( real ) ( ext-real real V65() ) number ) .[ : ( ( ) ( complex-membered ext-real-membered real-membered open non left_end non right_end bounded_below bounded_above real-bounded interval ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ;

theorem :: RCOMP_3:42
for r, s, a, b being ( ( real ) ( ext-real real V65() ) number ) st r : ( ( real ) ( ext-real real V65() ) number ) <= s : ( ( real ) ( ext-real real V65() ) number ) holds
for X being ( ( ) ( complex-membered ext-real-membered real-membered ) Subset of ) st X : ( ( ) ( complex-membered ext-real-membered real-membered ) Subset of ) = ].a : ( ( real ) ( ext-real real V65() ) number ) ,b : ( ( real ) ( ext-real real V65() ) number ) .] : ( ( ) ( complex-membered ext-real-membered real-membered non left_end bounded_below bounded_above real-bounded interval ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) & r : ( ( real ) ( ext-real real V65() ) number ) <= a : ( ( real ) ( ext-real real V65() ) number ) & b : ( ( real ) ( ext-real real V65() ) number ) < s : ( ( real ) ( ext-real real V65() ) number ) holds
Int X : ( ( ) ( complex-membered ext-real-membered real-membered ) Subset of ) : ( ( ) ( open complex-membered ext-real-membered real-membered ) Element of K32( the carrier of (Closed-Interval-TSpace (b1 : ( ( real ) ( ext-real real V65() ) number ) ,b2 : ( ( real ) ( ext-real real V65() ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like real-membered ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 T_2 real-membered ) TopStruct ) ) : ( ( ) ( non empty complex-membered ext-real-membered real-membered ) set ) ) : ( ( ) ( non empty ) set ) ) = ].a : ( ( real ) ( ext-real real V65() ) number ) ,b : ( ( real ) ( ext-real real V65() ) number ) .[ : ( ( ) ( complex-membered ext-real-membered real-membered open non left_end non right_end bounded_below bounded_above real-bounded interval ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ;

theorem :: RCOMP_3:43
for r, s being ( ( real ) ( ext-real real V65() ) number )
for X being ( ( ) ( complex-membered ext-real-membered real-membered ) Subset of )
for Y being ( ( ) ( complex-membered ext-real-membered real-membered ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) st X : ( ( ) ( complex-membered ext-real-membered real-membered ) Subset of ) = Y : ( ( ) ( complex-membered ext-real-membered real-membered ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) holds
( X : ( ( ) ( complex-membered ext-real-membered real-membered ) Subset of ) is connected iff Y : ( ( ) ( complex-membered ext-real-membered real-membered ) Subset of ( ( ) ( non empty non trivial non finite ) set ) ) is interval ) ;

registration
let T be ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ;
cluster open closed connected for ( ( ) ( ) Element of K32( the carrier of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ;
end;

registration
let T be ( ( non empty TopSpace-like connected ) ( non empty TopSpace-like connected ) TopSpace) ;
cluster non empty open closed connected for ( ( ) ( ) Element of K32( the carrier of T : ( ( non empty TopSpace-like connected ) ( non empty TopSpace-like connected ) TopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ;
end;

theorem :: RCOMP_3:44
for r, s being ( ( real ) ( ext-real real V65() ) number ) st r : ( ( real ) ( ext-real real V65() ) number ) <= s : ( ( real ) ( ext-real real V65() ) number ) holds
for X being ( ( open connected ) ( open connected complex-membered ext-real-membered real-membered ) Subset of ) holds
( X : ( ( open connected ) ( open connected complex-membered ext-real-membered real-membered ) Subset of ) is empty or X : ( ( open connected ) ( open connected complex-membered ext-real-membered real-membered ) Subset of ) = [.r : ( ( real ) ( ext-real real V65() ) number ) ,s : ( ( real ) ( ext-real real V65() ) number ) .] : ( ( ) ( complex-membered ext-real-membered real-membered closed bounded_below bounded_above real-bounded interval ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) or ex a being ( ( real ) ( ext-real real V65() ) number ) st
( r : ( ( real ) ( ext-real real V65() ) number ) < a : ( ( real ) ( ext-real real V65() ) number ) & a : ( ( real ) ( ext-real real V65() ) number ) <= s : ( ( real ) ( ext-real real V65() ) number ) & X : ( ( open connected ) ( open connected complex-membered ext-real-membered real-membered ) Subset of ) = [.r : ( ( real ) ( ext-real real V65() ) number ) ,a : ( ( real ) ( ext-real real V65() ) number ) .[ : ( ( ) ( complex-membered ext-real-membered real-membered non right_end bounded_below bounded_above real-bounded interval ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) or ex a being ( ( real ) ( ext-real real V65() ) number ) st
( r : ( ( real ) ( ext-real real V65() ) number ) <= a : ( ( real ) ( ext-real real V65() ) number ) & a : ( ( real ) ( ext-real real V65() ) number ) < s : ( ( real ) ( ext-real real V65() ) number ) & X : ( ( open connected ) ( open connected complex-membered ext-real-membered real-membered ) Subset of ) = ].a : ( ( real ) ( ext-real real V65() ) number ) ,s : ( ( real ) ( ext-real real V65() ) number ) .] : ( ( ) ( complex-membered ext-real-membered real-membered non left_end bounded_below bounded_above real-bounded interval ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) or ex a, b being ( ( real ) ( ext-real real V65() ) number ) st
( r : ( ( real ) ( ext-real real V65() ) number ) <= a : ( ( real ) ( ext-real real V65() ) number ) & a : ( ( real ) ( ext-real real V65() ) number ) < b : ( ( real ) ( ext-real real V65() ) number ) & b : ( ( real ) ( ext-real real V65() ) number ) <= s : ( ( real ) ( ext-real real V65() ) number ) & X : ( ( open connected ) ( open connected complex-membered ext-real-membered real-membered ) Subset of ) = ].a : ( ( real ) ( ext-real real V65() ) number ) ,b : ( ( real ) ( ext-real real V65() ) number ) .[ : ( ( ) ( complex-membered ext-real-membered real-membered open non left_end non right_end bounded_below bounded_above real-bounded interval ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) ) ;

begin

theorem :: RCOMP_3:45
for T being ( ( ) ( ) 1-sorted )
for F being ( ( finite ) ( finite ) Subset-Family of )
for F1 being ( ( ) ( ) Subset-Family of ) st F : ( ( finite ) ( finite ) Subset-Family of ) is ( ( ) ( ) Cover of ( ( ) ( ) set ) ) & F1 : ( ( ) ( ) Subset-Family of ) = F : ( ( finite ) ( finite ) Subset-Family of ) \ { X : ( ( ) ( ) Subset of ) where X is ( ( ) ( ) Subset of ) : ( X : ( ( ) ( ) Subset of ) in F : ( ( finite ) ( finite ) Subset-Family of ) & ex Y being ( ( ) ( ) Subset of ) st
( Y : ( ( ) ( ) Subset of ) in F : ( ( finite ) ( finite ) Subset-Family of ) & X : ( ( ) ( ) Subset of ) c< Y : ( ( ) ( ) Subset of ) ) ) } : ( ( ) ( finite ) Element of K32(K32( the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) holds
F1 : ( ( ) ( ) Subset-Family of ) is ( ( ) ( ) Cover of ( ( ) ( ) set ) ) ;

theorem :: RCOMP_3:46
for S being ( ( 1 : ( ( ) ( ordinal natural non empty ext-real positive non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) -element ) ( non empty trivial finite 1 : ( ( ) ( ordinal natural non empty ext-real positive non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) -element ) 1-sorted )
for s being ( ( ) ( ) Point of ( ( ) ( non empty trivial finite 1 : ( ( ) ( ordinal natural non empty ext-real positive non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) -element ) set ) )
for F being ( ( ) ( ) Subset-Family of ) st F : ( ( ) ( ) Subset-Family of ) is ( ( ) ( ) Cover of ( ( ) ( non empty trivial finite 1 : ( ( ) ( ordinal natural non empty ext-real positive non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) -element ) set ) ) holds
{s : ( ( ) ( ) Point of ( ( ) ( non empty trivial finite 1 : ( ( ) ( ordinal natural non empty ext-real positive non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) -element ) set ) ) } : ( ( ) ( non empty trivial finite 1 : ( ( ) ( ordinal natural non empty ext-real positive non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) -element ) set ) in F : ( ( ) ( ) Subset-Family of ) ;

definition
let T be ( ( ) ( ) TopStruct ) ;
let F be ( ( ) ( ) Subset-Family of ) ;
attr F is connected means :: RCOMP_3:def 1
 for X being ( ( ) ( ) Subset of ) st X : ( ( ) ( ) Subset of ) in F : ( ( non empty ) ( non empty ) set ) holds
X : ( ( ) ( ) Subset of ) is connected ;
end;

registration
let T be ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ;
cluster non empty open closed connected for ( ( ) ( ) Element of K32(K32( the carrier of T : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ;
end;

theorem :: RCOMP_3:47
for L being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace)
for G, G1 being ( ( ) ( ) Subset-Family of ) st G : ( ( ) ( ) Subset-Family of ) is ( ( ) ( ) Cover of ( ( ) ( ) set ) ) & G : ( ( ) ( ) Subset-Family of ) is finite holds
for ALL being ( ( ) ( ) set ) st G1 : ( ( ) ( ) Subset-Family of ) = G : ( ( ) ( ) Subset-Family of ) \ { X : ( ( ) ( ) Subset-Family of ) where X is ( ( ) ( ) Subset of ) : ( X : ( ( ) ( ) Subset-Family of ) in G : ( ( ) ( ) Subset-Family of ) & ex Y being ( ( ) ( ) Subset of ) st
( Y : ( ( ) ( ) Subset of ) in G : ( ( ) ( ) Subset-Family of ) & X : ( ( ) ( ) Subset-Family of ) c< Y : ( ( ) ( ) Subset of ) ) ) } : ( ( ) ( ) Element of K32(K32( the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) & ALL : ( ( ) ( ) set ) = { C : ( ( ) ( ) Subset-Family of ) where C is ( ( ) ( ) Subset-Family of ) : ( C : ( ( ) ( ) Subset-Family of ) is ( ( ) ( ) Cover of ( ( ) ( ) set ) ) & C : ( ( ) ( ) Subset-Family of ) c= G1 : ( ( ) ( ) Subset-Family of ) ) } holds
ALL : ( ( ) ( ) set ) has_lower_Zorn_property_wrt RelIncl ALL : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like reflexive antisymmetric transitive ) set ) ;

theorem :: RCOMP_3:48
for L being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace)
for G, ALL being ( ( ) ( ) set ) st ALL : ( ( ) ( ) set ) = { C : ( ( ) ( ) set ) where C is ( ( ) ( ) Subset-Family of ) : ( C : ( ( ) ( ) set ) is ( ( ) ( ) Cover of ( ( ) ( ) set ) ) & C : ( ( ) ( ) set ) c= G : ( ( ) ( ) set ) ) } holds
for M being ( ( ) ( ) set ) st M : ( ( ) ( ) set ) is_minimal_in RelIncl ALL : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like reflexive antisymmetric transitive ) set ) & M : ( ( ) ( ) set ) in field (RelIncl ALL : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like reflexive antisymmetric transitive ) set ) : ( ( ) ( ) set ) holds
for A1 being ( ( ) ( ) Subset of ) st A1 : ( ( ) ( ) Subset of ) in M : ( ( ) ( ) set ) holds
for A2, A3 being ( ( ) ( ) Subset of ) holds
( not A2 : ( ( ) ( ) Subset of ) in M : ( ( ) ( ) set ) or not A3 : ( ( ) ( ) Subset of ) in M : ( ( ) ( ) set ) or not A1 : ( ( ) ( ) Subset of ) c= A2 : ( ( ) ( ) Subset of ) \/ A3 : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K32( the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) or not A1 : ( ( ) ( ) Subset of ) <> A2 : ( ( ) ( ) Subset of ) or not A1 : ( ( ) ( ) Subset of ) <> A3 : ( ( ) ( ) Subset of ) ) ;

definition
let r, s be ( ( real ) ( ext-real real V65() ) number ) ;
let F be ( ( ) ( ) Subset-Family of ) ;
assume that
F : ( ( ) ( ) Subset-Family of ) is ( ( ) ( ) Cover of ( ( ) ( non empty complex-membered ext-real-membered real-membered ) set ) ) and
F : ( ( ) ( ) Subset-Family of ) is open and
F : ( ( ) ( ) Subset-Family of ) is connected and
r : ( ( real ) ( ext-real real V65() ) number ) <= s : ( ( real ) ( ext-real real V65() ) number ) ;
mode IntervalCover of F -> ( ( ) ( Relation-like NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) means :: RCOMP_3:def 2
( rng it : ( ( ) ( ) Element of r : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( ) Element of K32((bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) c= F : ( ( ) ( ) Element of r : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) & union (rng it : ( ( ) ( ) Element of r : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) ) : ( ( ) ( ) Element of K32((bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( complex-membered ext-real-membered real-membered ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) = [.r : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ,s : ( ( non empty ) ( non empty ) set ) .] : ( ( ) ( complex-membered ext-real-membered real-membered ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) & ( for n being ( ( natural ) ( ordinal natural ext-real non negative finite cardinal real V65() V66() ) Nat) st 1 : ( ( ) ( ordinal natural non empty ext-real positive non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) <= n : ( ( natural ) ( ordinal natural ext-real non negative finite cardinal real V65() V66() ) Nat) holds
( ( n : ( ( natural ) ( ordinal natural ext-real non negative finite cardinal real V65() V66() ) Nat) <= len it : ( ( ) ( ) Element of r : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( ordinal natural ext-real non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) implies not it : ( ( ) ( ) Element of r : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) /. n : ( ( natural ) ( ordinal natural ext-real non negative finite cardinal real V65() V66() ) Nat) : ( ( ) ( complex-membered ext-real-membered real-membered ) Element of bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) is empty ) & ( n : ( ( natural ) ( ordinal natural ext-real non negative finite cardinal real V65() V66() ) Nat) + 1 : ( ( ) ( ordinal natural non empty ext-real positive non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) : ( ( ) ( ordinal natural non empty ext-real positive non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) <= len it : ( ( ) ( ) Element of r : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( ordinal natural ext-real non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) implies ( lower_bound (it : ( ( ) ( ) Element of r : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) /. n : ( ( natural ) ( ordinal natural ext-real non negative finite cardinal real V65() V66() ) Nat) ) : ( ( ) ( complex-membered ext-real-membered real-membered ) Element of bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) : ( ( ) ( ext-real real V65() ) Element of REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) <= lower_bound (it : ( ( ) ( ) Element of r : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) /. (n : ( ( natural ) ( ordinal natural ext-real non negative finite cardinal real V65() V66() ) Nat) + 1 : ( ( ) ( ordinal natural non empty ext-real positive non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) ) : ( ( ) ( ordinal natural non empty ext-real positive non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) ) : ( ( ) ( complex-membered ext-real-membered real-membered ) Element of bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) : ( ( ) ( ext-real real V65() ) Element of REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) & upper_bound (it : ( ( ) ( ) Element of r : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) /. n : ( ( natural ) ( ordinal natural ext-real non negative finite cardinal real V65() V66() ) Nat) ) : ( ( ) ( complex-membered ext-real-membered real-membered ) Element of bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) : ( ( ) ( ext-real real V65() ) Element of REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) <= upper_bound (it : ( ( ) ( ) Element of r : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) /. (n : ( ( natural ) ( ordinal natural ext-real non negative finite cardinal real V65() V66() ) Nat) + 1 : ( ( ) ( ordinal natural non empty ext-real positive non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) ) : ( ( ) ( ordinal natural non empty ext-real positive non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) ) : ( ( ) ( complex-membered ext-real-membered real-membered ) Element of bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) : ( ( ) ( ext-real real V65() ) Element of REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) & lower_bound (it : ( ( ) ( ) Element of r : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) /. (n : ( ( natural ) ( ordinal natural ext-real non negative finite cardinal real V65() V66() ) Nat) + 1 : ( ( ) ( ordinal natural non empty ext-real positive non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) ) : ( ( ) ( ordinal natural non empty ext-real positive non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) ) : ( ( ) ( complex-membered ext-real-membered real-membered ) Element of bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) : ( ( ) ( ext-real real V65() ) Element of REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) < upper_bound (it : ( ( ) ( ) Element of r : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) /. n : ( ( natural ) ( ordinal natural ext-real non negative finite cardinal real V65() V66() ) Nat) ) : ( ( ) ( complex-membered ext-real-membered real-membered ) Element of bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) : ( ( ) ( ext-real real V65() ) Element of REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) ) ) & ( n : ( ( natural ) ( ordinal natural ext-real non negative finite cardinal real V65() V66() ) Nat) + 2 : ( ( ) ( ordinal natural non empty ext-real positive non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) : ( ( ) ( ordinal natural non empty ext-real positive non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) <= len it : ( ( ) ( ) Element of r : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( ordinal natural ext-real non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) implies upper_bound (it : ( ( ) ( ) Element of r : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) /. n : ( ( natural ) ( ordinal natural ext-real non negative finite cardinal real V65() V66() ) Nat) ) : ( ( ) ( complex-membered ext-real-membered real-membered ) Element of bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) : ( ( ) ( ext-real real V65() ) Element of REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) <= lower_bound (it : ( ( ) ( ) Element of r : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) /. (n : ( ( natural ) ( ordinal natural ext-real non negative finite cardinal real V65() V66() ) Nat) + 2 : ( ( ) ( ordinal natural non empty ext-real positive non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) ) : ( ( ) ( ordinal natural non empty ext-real positive non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) ) : ( ( ) ( complex-membered ext-real-membered real-membered ) Element of bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) : ( ( ) ( ext-real real V65() ) Element of REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) ) ) ) & ( [.r : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ,s : ( ( non empty ) ( non empty ) set ) .] : ( ( ) ( complex-membered ext-real-membered real-membered ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) in F : ( ( ) ( ) Element of r : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) implies it : ( ( ) ( ) Element of r : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) = <*[.r : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ,s : ( ( non empty ) ( non empty ) set ) .] : ( ( ) ( complex-membered ext-real-membered real-membered ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) *> : ( ( ) ( Relation-like NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) -valued Function-like non empty trivial finite 1 : ( ( ) ( ordinal natural non empty ext-real positive non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) -element FinSequence-like FinSubsequence-like ) FinSequence of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) & ( not [.r : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ,s : ( ( non empty ) ( non empty ) set ) .] : ( ( ) ( complex-membered ext-real-membered real-membered ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) in F : ( ( ) ( ) Element of r : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) implies ( ex p being ( ( real ) ( ext-real real V65() ) number ) st
( r : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) < p : ( ( natural ) ( ordinal natural ext-real non negative finite cardinal real V65() V66() ) Nat) & p : ( ( natural ) ( ordinal natural ext-real non negative finite cardinal real V65() V66() ) Nat) <= s : ( ( non empty ) ( non empty ) set ) & it : ( ( ) ( ) Element of r : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) . 1 : ( ( ) ( ordinal natural non empty ext-real positive non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) : ( ( ) ( ) set ) = [.r : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ,p : ( ( natural ) ( ordinal natural ext-real non negative finite cardinal real V65() V66() ) Nat) .[ : ( ( ) ( complex-membered ext-real-membered real-membered ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) & ex p being ( ( real ) ( ext-real real V65() ) number ) st
( r : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) <= p : ( ( natural ) ( ordinal natural ext-real non negative finite cardinal real V65() V66() ) Nat) & p : ( ( natural ) ( ordinal natural ext-real non negative finite cardinal real V65() V66() ) Nat) < s : ( ( non empty ) ( non empty ) set ) & it : ( ( ) ( ) Element of r : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) . (len it : ( ( ) ( ) Element of r : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) ) : ( ( ) ( ordinal natural ext-real non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) : ( ( ) ( ) set ) = ].p : ( ( natural ) ( ordinal natural ext-real non negative finite cardinal real V65() V66() ) Nat) ,s : ( ( non empty ) ( non empty ) set ) .] : ( ( ) ( complex-membered ext-real-membered real-membered ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) & ( for n being ( ( natural ) ( ordinal natural ext-real non negative finite cardinal real V65() V66() ) Nat) st 1 : ( ( ) ( ordinal natural non empty ext-real positive non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) < n : ( ( natural ) ( ordinal natural ext-real non negative finite cardinal real V65() V66() ) Nat) & n : ( ( natural ) ( ordinal natural ext-real non negative finite cardinal real V65() V66() ) Nat) < len it : ( ( ) ( ) Element of r : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( ordinal natural ext-real non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) holds
ex p, q being ( ( real ) ( ext-real real V65() ) number ) st
( r : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) <= p : ( ( real ) ( ext-real real V65() ) number ) & p : ( ( real ) ( ext-real real V65() ) number ) < q : ( ( real ) ( ext-real real V65() ) number ) & q : ( ( real ) ( ext-real real V65() ) number ) <= s : ( ( non empty ) ( non empty ) set ) & it : ( ( ) ( ) Element of r : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) . n : ( ( natural ) ( ordinal natural ext-real non negative finite cardinal real V65() V66() ) Nat) : ( ( ) ( ) set ) = ].p : ( ( real ) ( ext-real real V65() ) number ) ,q : ( ( real ) ( ext-real real V65() ) number ) .[ : ( ( ) ( complex-membered ext-real-membered real-membered open non left_end non right_end bounded_below bounded_above real-bounded interval ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) ) ) ) );
end;

theorem :: RCOMP_3:49
for r, s being ( ( real ) ( ext-real real V65() ) number )
for F being ( ( ) ( ) Subset-Family of ) st F : ( ( ) ( ) Subset-Family of ) is ( ( ) ( ) Cover of ( ( ) ( non empty complex-membered ext-real-membered real-membered ) set ) ) & F : ( ( ) ( ) Subset-Family of ) is open & F : ( ( ) ( ) Subset-Family of ) is connected & r : ( ( real ) ( ext-real real V65() ) number ) <= s : ( ( real ) ( ext-real real V65() ) number ) & [.r : ( ( real ) ( ext-real real V65() ) number ) ,s : ( ( real ) ( ext-real real V65() ) number ) .] : ( ( ) ( complex-membered ext-real-membered real-membered closed bounded_below bounded_above real-bounded interval ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) in F : ( ( ) ( ) Subset-Family of ) holds
<*[.r : ( ( real ) ( ext-real real V65() ) number ) ,s : ( ( real ) ( ext-real real V65() ) number ) .] : ( ( ) ( complex-membered ext-real-membered real-membered closed bounded_below bounded_above real-bounded interval ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) *> : ( ( ) ( Relation-like NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) -valued Function-like non empty trivial finite 1 : ( ( ) ( ordinal natural non empty ext-real positive non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) -element FinSequence-like FinSubsequence-like ) FinSequence of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) is ( ( ) ( Relation-like NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) IntervalCover of F : ( ( ) ( ) Subset-Family of ) ) ;

theorem :: RCOMP_3:50
for r being ( ( real ) ( ext-real real V65() ) number )
for F being ( ( ) ( finite V43() ) Subset-Family of )
for C being ( ( ) ( Relation-like NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) IntervalCover of F : ( ( ) ( finite V43() ) Subset-Family of ) ) st F : ( ( ) ( finite V43() ) Subset-Family of ) is ( ( ) ( ) Cover of ( ( ) ( non empty trivial finite 1 : ( ( ) ( ordinal natural non empty ext-real positive non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) -element complex-membered ext-real-membered real-membered left_end right_end bounded_below bounded_above real-bounded ) set ) ) & F : ( ( ) ( finite V43() ) Subset-Family of ) is open & F : ( ( ) ( finite V43() ) Subset-Family of ) is connected holds
C : ( ( ) ( Relation-like NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) IntervalCover of b2 : ( ( ) ( finite V43() ) Subset-Family of ) ) = <*[.r : ( ( real ) ( ext-real real V65() ) number ) ,r : ( ( real ) ( ext-real real V65() ) number ) .] : ( ( ) ( non empty complex-membered ext-real-membered real-membered closed bounded_below bounded_above real-bounded interval ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) *> : ( ( ) ( Relation-like NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) -valued Function-like non empty trivial finite 1 : ( ( ) ( ordinal natural non empty ext-real positive non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) -element FinSequence-like FinSubsequence-like ) FinSequence of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ;

theorem :: RCOMP_3:51
for r, s being ( ( real ) ( ext-real real V65() ) number )
for F being ( ( ) ( ) Subset-Family of )
for C being ( ( ) ( Relation-like NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) IntervalCover of F : ( ( ) ( ) Subset-Family of ) ) st F : ( ( ) ( ) Subset-Family of ) is ( ( ) ( ) Cover of ( ( ) ( non empty complex-membered ext-real-membered real-membered ) set ) ) & F : ( ( ) ( ) Subset-Family of ) is open & F : ( ( ) ( ) Subset-Family of ) is connected & r : ( ( real ) ( ext-real real V65() ) number ) <= s : ( ( real ) ( ext-real real V65() ) number ) holds
1 : ( ( ) ( ordinal natural non empty ext-real positive non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) <= len C : ( ( ) ( Relation-like NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) IntervalCover of b3 : ( ( ) ( ) Subset-Family of ) ) : ( ( ) ( ordinal natural ext-real non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) ;

theorem :: RCOMP_3:52
for r, s being ( ( real ) ( ext-real real V65() ) number )
for F being ( ( ) ( ) Subset-Family of )
for C being ( ( ) ( Relation-like NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) IntervalCover of F : ( ( ) ( ) Subset-Family of ) ) st F : ( ( ) ( ) Subset-Family of ) is ( ( ) ( ) Cover of ( ( ) ( non empty complex-membered ext-real-membered real-membered ) set ) ) & F : ( ( ) ( ) Subset-Family of ) is open & F : ( ( ) ( ) Subset-Family of ) is connected & r : ( ( real ) ( ext-real real V65() ) number ) <= s : ( ( real ) ( ext-real real V65() ) number ) & len C : ( ( ) ( Relation-like NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) IntervalCover of b3 : ( ( ) ( ) Subset-Family of ) ) : ( ( ) ( ordinal natural ext-real non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) = 1 : ( ( ) ( ordinal natural non empty ext-real positive non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) holds
C : ( ( ) ( Relation-like NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) IntervalCover of b3 : ( ( ) ( ) Subset-Family of ) ) = <*[.r : ( ( real ) ( ext-real real V65() ) number ) ,s : ( ( real ) ( ext-real real V65() ) number ) .] : ( ( ) ( complex-membered ext-real-membered real-membered closed bounded_below bounded_above real-bounded interval ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) *> : ( ( ) ( Relation-like NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) -valued Function-like non empty trivial finite 1 : ( ( ) ( ordinal natural non empty ext-real positive non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) -element FinSequence-like FinSubsequence-like ) FinSequence of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ;

theorem :: RCOMP_3:53
for r, s being ( ( real ) ( ext-real real V65() ) number )
for n, m being ( ( natural ) ( ordinal natural ext-real non negative finite cardinal real V65() V66() ) Nat)
for F being ( ( ) ( ) Subset-Family of )
for C being ( ( ) ( Relation-like NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) IntervalCover of F : ( ( ) ( ) Subset-Family of ) ) st F : ( ( ) ( ) Subset-Family of ) is ( ( ) ( ) Cover of ( ( ) ( non empty complex-membered ext-real-membered real-membered ) set ) ) & F : ( ( ) ( ) Subset-Family of ) is open & F : ( ( ) ( ) Subset-Family of ) is connected & r : ( ( real ) ( ext-real real V65() ) number ) <= s : ( ( real ) ( ext-real real V65() ) number ) & n : ( ( natural ) ( ordinal natural ext-real non negative finite cardinal real V65() V66() ) Nat) in dom C : ( ( ) ( Relation-like NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) IntervalCover of b5 : ( ( ) ( ) Subset-Family of ) ) : ( ( ) ( finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded ) Element of K32(NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) & m : ( ( natural ) ( ordinal natural ext-real non negative finite cardinal real V65() V66() ) Nat) in dom C : ( ( ) ( Relation-like NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) IntervalCover of b5 : ( ( ) ( ) Subset-Family of ) ) : ( ( ) ( finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded ) Element of K32(NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) & n : ( ( natural ) ( ordinal natural ext-real non negative finite cardinal real V65() V66() ) Nat) < m : ( ( natural ) ( ordinal natural ext-real non negative finite cardinal real V65() V66() ) Nat) holds
lower_bound (C : ( ( ) ( Relation-like NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) IntervalCover of b5 : ( ( ) ( ) Subset-Family of ) ) /. n : ( ( natural ) ( ordinal natural ext-real non negative finite cardinal real V65() V66() ) Nat) ) : ( ( ) ( complex-membered ext-real-membered real-membered ) Element of bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) : ( ( ) ( ext-real real V65() ) Element of REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) <= lower_bound (C : ( ( ) ( Relation-like NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) IntervalCover of b5 : ( ( ) ( ) Subset-Family of ) ) /. m : ( ( natural ) ( ordinal natural ext-real non negative finite cardinal real V65() V66() ) Nat) ) : ( ( ) ( complex-membered ext-real-membered real-membered ) Element of bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) : ( ( ) ( ext-real real V65() ) Element of REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) ;

theorem :: RCOMP_3:54
for r, s being ( ( real ) ( ext-real real V65() ) number )
for n, m being ( ( natural ) ( ordinal natural ext-real non negative finite cardinal real V65() V66() ) Nat)
for F being ( ( ) ( ) Subset-Family of )
for C being ( ( ) ( Relation-like NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) IntervalCover of F : ( ( ) ( ) Subset-Family of ) ) st F : ( ( ) ( ) Subset-Family of ) is ( ( ) ( ) Cover of ( ( ) ( non empty complex-membered ext-real-membered real-membered ) set ) ) & F : ( ( ) ( ) Subset-Family of ) is open & F : ( ( ) ( ) Subset-Family of ) is connected & r : ( ( real ) ( ext-real real V65() ) number ) <= s : ( ( real ) ( ext-real real V65() ) number ) & n : ( ( natural ) ( ordinal natural ext-real non negative finite cardinal real V65() V66() ) Nat) in dom C : ( ( ) ( Relation-like NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) IntervalCover of b5 : ( ( ) ( ) Subset-Family of ) ) : ( ( ) ( finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded ) Element of K32(NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) & m : ( ( natural ) ( ordinal natural ext-real non negative finite cardinal real V65() V66() ) Nat) in dom C : ( ( ) ( Relation-like NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) IntervalCover of b5 : ( ( ) ( ) Subset-Family of ) ) : ( ( ) ( finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded ) Element of K32(NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) & n : ( ( natural ) ( ordinal natural ext-real non negative finite cardinal real V65() V66() ) Nat) < m : ( ( natural ) ( ordinal natural ext-real non negative finite cardinal real V65() V66() ) Nat) holds
upper_bound (C : ( ( ) ( Relation-like NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) IntervalCover of b5 : ( ( ) ( ) Subset-Family of ) ) /. n : ( ( natural ) ( ordinal natural ext-real non negative finite cardinal real V65() V66() ) Nat) ) : ( ( ) ( complex-membered ext-real-membered real-membered ) Element of bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) : ( ( ) ( ext-real real V65() ) Element of REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) <= upper_bound (C : ( ( ) ( Relation-like NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) IntervalCover of b5 : ( ( ) ( ) Subset-Family of ) ) /. m : ( ( natural ) ( ordinal natural ext-real non negative finite cardinal real V65() V66() ) Nat) ) : ( ( ) ( complex-membered ext-real-membered real-membered ) Element of bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) : ( ( ) ( ext-real real V65() ) Element of REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) ;

theorem :: RCOMP_3:55
for r, s being ( ( real ) ( ext-real real V65() ) number )
for n being ( ( natural ) ( ordinal natural ext-real non negative finite cardinal real V65() V66() ) Nat)
for F being ( ( ) ( ) Subset-Family of )
for C being ( ( ) ( Relation-like NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) IntervalCover of F : ( ( ) ( ) Subset-Family of ) ) st F : ( ( ) ( ) Subset-Family of ) is ( ( ) ( ) Cover of ( ( ) ( non empty complex-membered ext-real-membered real-membered ) set ) ) & F : ( ( ) ( ) Subset-Family of ) is open & F : ( ( ) ( ) Subset-Family of ) is connected & r : ( ( real ) ( ext-real real V65() ) number ) <= s : ( ( real ) ( ext-real real V65() ) number ) & 1 : ( ( ) ( ordinal natural non empty ext-real positive non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) <= n : ( ( natural ) ( ordinal natural ext-real non negative finite cardinal real V65() V66() ) Nat) & n : ( ( natural ) ( ordinal natural ext-real non negative finite cardinal real V65() V66() ) Nat) + 1 : ( ( ) ( ordinal natural non empty ext-real positive non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) : ( ( ) ( ordinal natural non empty ext-real positive non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) <= len C : ( ( ) ( Relation-like NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) IntervalCover of b4 : ( ( ) ( ) Subset-Family of ) ) : ( ( ) ( ordinal natural ext-real non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) holds
not ].(lower_bound (C : ( ( ) ( Relation-like NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) IntervalCover of b4 : ( ( ) ( ) Subset-Family of ) ) /. (n : ( ( natural ) ( ordinal natural ext-real non negative finite cardinal real V65() V66() ) Nat) + 1 : ( ( ) ( ordinal natural non empty ext-real positive non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) ) : ( ( ) ( ordinal natural non empty ext-real positive non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) ) : ( ( ) ( complex-membered ext-real-membered real-membered ) Element of bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) ) : ( ( ) ( ext-real real V65() ) Element of REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) ,(upper_bound (C : ( ( ) ( Relation-like NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) IntervalCover of b4 : ( ( ) ( ) Subset-Family of ) ) /. n : ( ( natural ) ( ordinal natural ext-real non negative finite cardinal real V65() V66() ) Nat) ) : ( ( ) ( complex-membered ext-real-membered real-membered ) Element of bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) ) : ( ( ) ( ext-real real V65() ) Element of REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) .[ : ( ( ) ( complex-membered ext-real-membered real-membered open non left_end non right_end bounded_below bounded_above real-bounded interval ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) is empty ;

theorem :: RCOMP_3:56
for r, s being ( ( real ) ( ext-real real V65() ) number )
for F being ( ( ) ( ) Subset-Family of )
for C being ( ( ) ( Relation-like NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) IntervalCover of F : ( ( ) ( ) Subset-Family of ) ) st F : ( ( ) ( ) Subset-Family of ) is ( ( ) ( ) Cover of ( ( ) ( non empty complex-membered ext-real-membered real-membered ) set ) ) & F : ( ( ) ( ) Subset-Family of ) is open & F : ( ( ) ( ) Subset-Family of ) is connected & r : ( ( real ) ( ext-real real V65() ) number ) <= s : ( ( real ) ( ext-real real V65() ) number ) holds
lower_bound (C : ( ( ) ( Relation-like NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) IntervalCover of b3 : ( ( ) ( ) Subset-Family of ) ) /. 1 : ( ( ) ( ordinal natural non empty ext-real positive non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) ) : ( ( ) ( complex-membered ext-real-membered real-membered ) Element of bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) : ( ( ) ( ext-real real V65() ) Element of REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) = r : ( ( real ) ( ext-real real V65() ) number ) ;

theorem :: RCOMP_3:57
for r, s being ( ( real ) ( ext-real real V65() ) number )
for F being ( ( ) ( ) Subset-Family of )
for C being ( ( ) ( Relation-like NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) IntervalCover of F : ( ( ) ( ) Subset-Family of ) ) st F : ( ( ) ( ) Subset-Family of ) is ( ( ) ( ) Cover of ( ( ) ( non empty complex-membered ext-real-membered real-membered ) set ) ) & F : ( ( ) ( ) Subset-Family of ) is open & F : ( ( ) ( ) Subset-Family of ) is connected & r : ( ( real ) ( ext-real real V65() ) number ) <= s : ( ( real ) ( ext-real real V65() ) number ) holds
r : ( ( real ) ( ext-real real V65() ) number ) in C : ( ( ) ( Relation-like NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) IntervalCover of b3 : ( ( ) ( ) Subset-Family of ) ) /. 1 : ( ( ) ( ordinal natural non empty ext-real positive non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) : ( ( ) ( complex-membered ext-real-membered real-membered ) Element of bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) ;

theorem :: RCOMP_3:58
for r, s being ( ( real ) ( ext-real real V65() ) number )
for F being ( ( ) ( ) Subset-Family of )
for C being ( ( ) ( Relation-like NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) IntervalCover of F : ( ( ) ( ) Subset-Family of ) ) st F : ( ( ) ( ) Subset-Family of ) is ( ( ) ( ) Cover of ( ( ) ( non empty complex-membered ext-real-membered real-membered ) set ) ) & F : ( ( ) ( ) Subset-Family of ) is open & F : ( ( ) ( ) Subset-Family of ) is connected & r : ( ( real ) ( ext-real real V65() ) number ) <= s : ( ( real ) ( ext-real real V65() ) number ) holds
upper_bound (C : ( ( ) ( Relation-like NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) IntervalCover of b3 : ( ( ) ( ) Subset-Family of ) ) /. (len C : ( ( ) ( Relation-like NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) IntervalCover of b3 : ( ( ) ( ) Subset-Family of ) ) ) : ( ( ) ( ordinal natural ext-real non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) ) : ( ( ) ( complex-membered ext-real-membered real-membered ) Element of bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) : ( ( ) ( ext-real real V65() ) Element of REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) = s : ( ( real ) ( ext-real real V65() ) number ) ;

theorem :: RCOMP_3:59
for r, s being ( ( real ) ( ext-real real V65() ) number )
for F being ( ( ) ( ) Subset-Family of )
for C being ( ( ) ( Relation-like NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) IntervalCover of F : ( ( ) ( ) Subset-Family of ) ) st F : ( ( ) ( ) Subset-Family of ) is ( ( ) ( ) Cover of ( ( ) ( non empty complex-membered ext-real-membered real-membered ) set ) ) & F : ( ( ) ( ) Subset-Family of ) is open & F : ( ( ) ( ) Subset-Family of ) is connected & r : ( ( real ) ( ext-real real V65() ) number ) <= s : ( ( real ) ( ext-real real V65() ) number ) holds
s : ( ( real ) ( ext-real real V65() ) number ) in C : ( ( ) ( Relation-like NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) IntervalCover of b3 : ( ( ) ( ) Subset-Family of ) ) /. (len C : ( ( ) ( Relation-like NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) IntervalCover of b3 : ( ( ) ( ) Subset-Family of ) ) ) : ( ( ) ( ordinal natural ext-real non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) : ( ( ) ( complex-membered ext-real-membered real-membered ) Element of bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) ;

definition
let r, s be ( ( real ) ( ext-real real V65() ) number ) ;
let F be ( ( ) ( ) Subset-Family of ) ;
let C be ( ( ) ( Relation-like NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) IntervalCover of F : ( ( ) ( ) Subset-Family of ) ) ;
assume ( F : ( ( ) ( ) Subset-Family of ) is ( ( ) ( ) Cover of ( ( ) ( non empty complex-membered ext-real-membered real-membered ) set ) ) & F : ( ( ) ( ) Subset-Family of ) is open & F : ( ( ) ( ) Subset-Family of ) is connected & r : ( ( real ) ( ext-real real V65() ) number ) <= s : ( ( real ) ( ext-real real V65() ) number ) ) ;
mode IntervalCoverPts of C -> ( ( ) ( Relation-like NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) -valued Function-like finite FinSequence-like FinSubsequence-like V124() V125() V126() ) FinSequence of REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) means :: RCOMP_3:def 3
( len it : ( ( ) ( ) Element of s : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ordinal natural ext-real non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) = (len C : ( ( ) ( ) Element of r : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) ) : ( ( ) ( ordinal natural ext-real non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) + 1 : ( ( ) ( ordinal natural non empty ext-real positive non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) : ( ( ) ( ordinal natural non empty ext-real positive non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) & it : ( ( ) ( ) Element of s : ( ( non empty ) ( non empty ) set ) ) . 1 : ( ( ) ( ordinal natural non empty ext-real positive non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) : ( ( ) ( ) set ) = r : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) & it : ( ( ) ( ) Element of s : ( ( non empty ) ( non empty ) set ) ) . (len it : ( ( ) ( ) Element of s : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ordinal natural ext-real non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) : ( ( ) ( ) set ) = s : ( ( non empty ) ( non empty ) set ) & ( for n being ( ( natural ) ( ordinal natural ext-real non negative finite cardinal real V65() V66() ) Nat) st 1 : ( ( ) ( ordinal natural non empty ext-real positive non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) <= n : ( ( natural ) ( ordinal natural ext-real non negative finite cardinal real V65() V66() ) Nat) & n : ( ( natural ) ( ordinal natural ext-real non negative finite cardinal real V65() V66() ) Nat) + 1 : ( ( ) ( ordinal natural non empty ext-real positive non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) : ( ( ) ( ordinal natural non empty ext-real positive non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) < len it : ( ( ) ( ) Element of s : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ordinal natural ext-real non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) holds
it : ( ( ) ( ) Element of s : ( ( non empty ) ( non empty ) set ) ) . (n : ( ( natural ) ( ordinal natural ext-real non negative finite cardinal real V65() V66() ) Nat) + 1 : ( ( ) ( ordinal natural non empty ext-real positive non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) ) : ( ( ) ( ordinal natural non empty ext-real positive non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) : ( ( ) ( ) set ) in ].(lower_bound (C : ( ( ) ( ) Element of r : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) /. (n : ( ( natural ) ( ordinal natural ext-real non negative finite cardinal real V65() V66() ) Nat) + 1 : ( ( ) ( ordinal natural non empty ext-real positive non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) ) : ( ( ) ( ordinal natural non empty ext-real positive non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) ) : ( ( ) ( complex-membered ext-real-membered real-membered ) Element of bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) ) : ( ( ) ( ext-real real V65() ) Element of REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) ,(upper_bound (C : ( ( ) ( ) Element of r : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) /. n : ( ( natural ) ( ordinal natural ext-real non negative finite cardinal real V65() V66() ) Nat) ) : ( ( ) ( complex-membered ext-real-membered real-membered ) Element of bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) ) : ( ( ) ( ext-real real V65() ) Element of REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) .[ : ( ( ) ( complex-membered ext-real-membered real-membered open non left_end non right_end bounded_below bounded_above real-bounded interval ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) );
end;

theorem :: RCOMP_3:60
for r, s being ( ( real ) ( ext-real real V65() ) number )
for F being ( ( ) ( ) Subset-Family of )
for C being ( ( ) ( Relation-like NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) IntervalCover of F : ( ( ) ( ) Subset-Family of ) )
for G being ( ( ) ( Relation-like NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) -valued Function-like finite FinSequence-like FinSubsequence-like V124() V125() V126() ) IntervalCoverPts of C : ( ( ) ( Relation-like NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) IntervalCover of b3 : ( ( ) ( ) Subset-Family of ) ) ) st F : ( ( ) ( ) Subset-Family of ) is ( ( ) ( ) Cover of ( ( ) ( non empty complex-membered ext-real-membered real-membered ) set ) ) & F : ( ( ) ( ) Subset-Family of ) is open & F : ( ( ) ( ) Subset-Family of ) is connected & r : ( ( real ) ( ext-real real V65() ) number ) <= s : ( ( real ) ( ext-real real V65() ) number ) holds
2 : ( ( ) ( ordinal natural non empty ext-real positive non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) <= len G : ( ( ) ( Relation-like NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) -valued Function-like finite FinSequence-like FinSubsequence-like V124() V125() V126() ) IntervalCoverPts of b4 : ( ( ) ( Relation-like NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) IntervalCover of b3 : ( ( ) ( ) Subset-Family of ) ) ) : ( ( ) ( ordinal natural ext-real non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) ;

theorem :: RCOMP_3:61
for r, s being ( ( real ) ( ext-real real V65() ) number )
for F being ( ( ) ( ) Subset-Family of )
for C being ( ( ) ( Relation-like NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) IntervalCover of F : ( ( ) ( ) Subset-Family of ) )
for G being ( ( ) ( Relation-like NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) -valued Function-like finite FinSequence-like FinSubsequence-like V124() V125() V126() ) IntervalCoverPts of C : ( ( ) ( Relation-like NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) IntervalCover of b3 : ( ( ) ( ) Subset-Family of ) ) ) st F : ( ( ) ( ) Subset-Family of ) is ( ( ) ( ) Cover of ( ( ) ( non empty complex-membered ext-real-membered real-membered ) set ) ) & F : ( ( ) ( ) Subset-Family of ) is open & F : ( ( ) ( ) Subset-Family of ) is connected & r : ( ( real ) ( ext-real real V65() ) number ) <= s : ( ( real ) ( ext-real real V65() ) number ) & len C : ( ( ) ( Relation-like NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) IntervalCover of b3 : ( ( ) ( ) Subset-Family of ) ) : ( ( ) ( ordinal natural ext-real non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) = 1 : ( ( ) ( ordinal natural non empty ext-real positive non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) holds
G : ( ( ) ( Relation-like NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) -valued Function-like finite FinSequence-like FinSubsequence-like V124() V125() V126() ) IntervalCoverPts of b4 : ( ( ) ( Relation-like NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) IntervalCover of b3 : ( ( ) ( ) Subset-Family of ) ) ) = <*r : ( ( real ) ( ext-real real V65() ) number ) ,s : ( ( real ) ( ext-real real V65() ) number ) *> : ( ( ) ( Relation-like NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined Function-like non empty finite 2 : ( ( ) ( ordinal natural non empty ext-real positive non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) -element FinSequence-like FinSubsequence-like ) set ) ;

theorem :: RCOMP_3:62
for r, s being ( ( real ) ( ext-real real V65() ) number )
for n being ( ( natural ) ( ordinal natural ext-real non negative finite cardinal real V65() V66() ) Nat)
for F being ( ( ) ( ) Subset-Family of )
for C being ( ( ) ( Relation-like NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) IntervalCover of F : ( ( ) ( ) Subset-Family of ) )
for G being ( ( ) ( Relation-like NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) -valued Function-like finite FinSequence-like FinSubsequence-like V124() V125() V126() ) IntervalCoverPts of C : ( ( ) ( Relation-like NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) IntervalCover of b4 : ( ( ) ( ) Subset-Family of ) ) ) st F : ( ( ) ( ) Subset-Family of ) is ( ( ) ( ) Cover of ( ( ) ( non empty complex-membered ext-real-membered real-membered ) set ) ) & F : ( ( ) ( ) Subset-Family of ) is open & F : ( ( ) ( ) Subset-Family of ) is connected & r : ( ( real ) ( ext-real real V65() ) number ) <= s : ( ( real ) ( ext-real real V65() ) number ) & 1 : ( ( ) ( ordinal natural non empty ext-real positive non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) <= n : ( ( natural ) ( ordinal natural ext-real non negative finite cardinal real V65() V66() ) Nat) & n : ( ( natural ) ( ordinal natural ext-real non negative finite cardinal real V65() V66() ) Nat) + 1 : ( ( ) ( ordinal natural non empty ext-real positive non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) : ( ( ) ( ordinal natural non empty ext-real positive non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) < len G : ( ( ) ( Relation-like NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) -valued Function-like finite FinSequence-like FinSubsequence-like V124() V125() V126() ) IntervalCoverPts of b5 : ( ( ) ( Relation-like NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) IntervalCover of b4 : ( ( ) ( ) Subset-Family of ) ) ) : ( ( ) ( ordinal natural ext-real non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) holds
G : ( ( ) ( Relation-like NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) -valued Function-like finite FinSequence-like FinSubsequence-like V124() V125() V126() ) IntervalCoverPts of b5 : ( ( ) ( Relation-like NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) IntervalCover of b4 : ( ( ) ( ) Subset-Family of ) ) ) . (n : ( ( natural ) ( ordinal natural ext-real non negative finite cardinal real V65() V66() ) Nat) + 1 : ( ( ) ( ordinal natural non empty ext-real positive non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) ) : ( ( ) ( ordinal natural non empty ext-real positive non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) : ( ( ) ( ext-real real V65() ) set ) < upper_bound (C : ( ( ) ( Relation-like NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) IntervalCover of b4 : ( ( ) ( ) Subset-Family of ) ) /. n : ( ( natural ) ( ordinal natural ext-real non negative finite cardinal real V65() V66() ) Nat) ) : ( ( ) ( complex-membered ext-real-membered real-membered ) Element of bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) : ( ( ) ( ext-real real V65() ) Element of REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) ;

theorem :: RCOMP_3:63
for r, s being ( ( real ) ( ext-real real V65() ) number )
for n being ( ( natural ) ( ordinal natural ext-real non negative finite cardinal real V65() V66() ) Nat)
for F being ( ( ) ( ) Subset-Family of )
for C being ( ( ) ( Relation-like NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) IntervalCover of F : ( ( ) ( ) Subset-Family of ) )
for G being ( ( ) ( Relation-like NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) -valued Function-like finite FinSequence-like FinSubsequence-like V124() V125() V126() ) IntervalCoverPts of C : ( ( ) ( Relation-like NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) IntervalCover of b4 : ( ( ) ( ) Subset-Family of ) ) ) st F : ( ( ) ( ) Subset-Family of ) is ( ( ) ( ) Cover of ( ( ) ( non empty complex-membered ext-real-membered real-membered ) set ) ) & F : ( ( ) ( ) Subset-Family of ) is open & F : ( ( ) ( ) Subset-Family of ) is connected & r : ( ( real ) ( ext-real real V65() ) number ) <= s : ( ( real ) ( ext-real real V65() ) number ) & 1 : ( ( ) ( ordinal natural non empty ext-real positive non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) < n : ( ( natural ) ( ordinal natural ext-real non negative finite cardinal real V65() V66() ) Nat) & n : ( ( natural ) ( ordinal natural ext-real non negative finite cardinal real V65() V66() ) Nat) <= len C : ( ( ) ( Relation-like NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) IntervalCover of b4 : ( ( ) ( ) Subset-Family of ) ) : ( ( ) ( ordinal natural ext-real non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) holds
lower_bound (C : ( ( ) ( Relation-like NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) IntervalCover of b4 : ( ( ) ( ) Subset-Family of ) ) /. n : ( ( natural ) ( ordinal natural ext-real non negative finite cardinal real V65() V66() ) Nat) ) : ( ( ) ( complex-membered ext-real-membered real-membered ) Element of bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) : ( ( ) ( ext-real real V65() ) Element of REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) < G : ( ( ) ( Relation-like NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) -valued Function-like finite FinSequence-like FinSubsequence-like V124() V125() V126() ) IntervalCoverPts of b5 : ( ( ) ( Relation-like NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) IntervalCover of b4 : ( ( ) ( ) Subset-Family of ) ) ) . n : ( ( natural ) ( ordinal natural ext-real non negative finite cardinal real V65() V66() ) Nat) : ( ( ) ( ext-real real V65() ) set ) ;

theorem :: RCOMP_3:64
for r, s being ( ( real ) ( ext-real real V65() ) number )
for n being ( ( natural ) ( ordinal natural ext-real non negative finite cardinal real V65() V66() ) Nat)
for F being ( ( ) ( ) Subset-Family of )
for C being ( ( ) ( Relation-like NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) IntervalCover of F : ( ( ) ( ) Subset-Family of ) )
for G being ( ( ) ( Relation-like NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) -valued Function-like finite FinSequence-like FinSubsequence-like V124() V125() V126() ) IntervalCoverPts of C : ( ( ) ( Relation-like NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) IntervalCover of b4 : ( ( ) ( ) Subset-Family of ) ) ) st F : ( ( ) ( ) Subset-Family of ) is ( ( ) ( ) Cover of ( ( ) ( non empty complex-membered ext-real-membered real-membered ) set ) ) & F : ( ( ) ( ) Subset-Family of ) is open & F : ( ( ) ( ) Subset-Family of ) is connected & r : ( ( real ) ( ext-real real V65() ) number ) <= s : ( ( real ) ( ext-real real V65() ) number ) & 1 : ( ( ) ( ordinal natural non empty ext-real positive non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) <= n : ( ( natural ) ( ordinal natural ext-real non negative finite cardinal real V65() V66() ) Nat) & n : ( ( natural ) ( ordinal natural ext-real non negative finite cardinal real V65() V66() ) Nat) < len C : ( ( ) ( Relation-like NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) IntervalCover of b4 : ( ( ) ( ) Subset-Family of ) ) : ( ( ) ( ordinal natural ext-real non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) holds
G : ( ( ) ( Relation-like NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) -valued Function-like finite FinSequence-like FinSubsequence-like V124() V125() V126() ) IntervalCoverPts of b5 : ( ( ) ( Relation-like NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) IntervalCover of b4 : ( ( ) ( ) Subset-Family of ) ) ) . n : ( ( natural ) ( ordinal natural ext-real non negative finite cardinal real V65() V66() ) Nat) : ( ( ) ( ext-real real V65() ) set ) <= lower_bound (C : ( ( ) ( Relation-like NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) IntervalCover of b4 : ( ( ) ( ) Subset-Family of ) ) /. (n : ( ( natural ) ( ordinal natural ext-real non negative finite cardinal real V65() V66() ) Nat) + 1 : ( ( ) ( ordinal natural non empty ext-real positive non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) ) : ( ( ) ( ordinal natural non empty ext-real positive non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) ) : ( ( ) ( complex-membered ext-real-membered real-membered ) Element of bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) : ( ( ) ( ext-real real V65() ) Element of REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) ;

theorem :: RCOMP_3:65
for r, s being ( ( real ) ( ext-real real V65() ) number )
for F being ( ( ) ( ) Subset-Family of )
for C being ( ( ) ( Relation-like NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) IntervalCover of F : ( ( ) ( ) Subset-Family of ) )
for G being ( ( ) ( Relation-like NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) -valued Function-like finite FinSequence-like FinSubsequence-like V124() V125() V126() ) IntervalCoverPts of C : ( ( ) ( Relation-like NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) IntervalCover of b3 : ( ( ) ( ) Subset-Family of ) ) ) st F : ( ( ) ( ) Subset-Family of ) is ( ( ) ( ) Cover of ( ( ) ( non empty complex-membered ext-real-membered real-membered ) set ) ) & F : ( ( ) ( ) Subset-Family of ) is open & F : ( ( ) ( ) Subset-Family of ) is connected & r : ( ( real ) ( ext-real real V65() ) number ) < s : ( ( real ) ( ext-real real V65() ) number ) holds
G : ( ( ) ( Relation-like NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) -valued Function-like finite FinSequence-like FinSubsequence-like V124() V125() V126() ) IntervalCoverPts of b4 : ( ( ) ( Relation-like NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) IntervalCover of b3 : ( ( ) ( ) Subset-Family of ) ) ) is increasing ;

theorem :: RCOMP_3:66
for r, s being ( ( real ) ( ext-real real V65() ) number )
for n being ( ( natural ) ( ordinal natural ext-real non negative finite cardinal real V65() V66() ) Nat)
for F being ( ( ) ( ) Subset-Family of )
for C being ( ( ) ( Relation-like NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) IntervalCover of F : ( ( ) ( ) Subset-Family of ) )
for G being ( ( ) ( Relation-like NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) -valued Function-like finite FinSequence-like FinSubsequence-like V124() V125() V126() ) IntervalCoverPts of C : ( ( ) ( Relation-like NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) IntervalCover of b4 : ( ( ) ( ) Subset-Family of ) ) ) st F : ( ( ) ( ) Subset-Family of ) is ( ( ) ( ) Cover of ( ( ) ( non empty complex-membered ext-real-membered real-membered ) set ) ) & F : ( ( ) ( ) Subset-Family of ) is open & F : ( ( ) ( ) Subset-Family of ) is connected & r : ( ( real ) ( ext-real real V65() ) number ) <= s : ( ( real ) ( ext-real real V65() ) number ) & 1 : ( ( ) ( ordinal natural non empty ext-real positive non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) <= n : ( ( natural ) ( ordinal natural ext-real non negative finite cardinal real V65() V66() ) Nat) & n : ( ( natural ) ( ordinal natural ext-real non negative finite cardinal real V65() V66() ) Nat) < len G : ( ( ) ( Relation-like NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) -valued Function-like finite FinSequence-like FinSubsequence-like V124() V125() V126() ) IntervalCoverPts of b5 : ( ( ) ( Relation-like NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) IntervalCover of b4 : ( ( ) ( ) Subset-Family of ) ) ) : ( ( ) ( ordinal natural ext-real non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) holds
[.(G : ( ( ) ( Relation-like NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) -valued Function-like finite FinSequence-like FinSubsequence-like V124() V125() V126() ) IntervalCoverPts of b5 : ( ( ) ( Relation-like NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) IntervalCover of b4 : ( ( ) ( ) Subset-Family of ) ) ) . n : ( ( natural ) ( ordinal natural ext-real non negative finite cardinal real V65() V66() ) Nat) ) : ( ( ) ( ext-real real V65() ) set ) ,(G : ( ( ) ( Relation-like NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) -valued Function-like finite FinSequence-like FinSubsequence-like V124() V125() V126() ) IntervalCoverPts of b5 : ( ( ) ( Relation-like NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) IntervalCover of b4 : ( ( ) ( ) Subset-Family of ) ) ) . (n : ( ( natural ) ( ordinal natural ext-real non negative finite cardinal real V65() V66() ) Nat) + 1 : ( ( ) ( ordinal natural non empty ext-real positive non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) ) : ( ( ) ( ordinal natural non empty ext-real positive non negative finite cardinal real V65() V66() V67() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) ) : ( ( ) ( ext-real real V65() ) set ) .] : ( ( ) ( complex-membered ext-real-membered real-membered closed bounded_below bounded_above real-bounded interval ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) c= C : ( ( ) ( Relation-like NAT : ( ( ) ( ordinal non trivial non with_non-empty_elements non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V123() bounded_below ) Element of K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined bool REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial non finite ) Element of K32(K32(REAL : ( ( ) ( non empty non trivial non with_non-empty_elements non finite complex-membered ext-real-membered real-membered V123() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) IntervalCover of b4 : ( ( ) ( ) Subset-Family of ) ) . n : ( ( natural ) ( ordinal natural ext-real non negative finite cardinal real V65() V66() ) Nat) : ( ( ) ( ) set ) ;