:: RCOMP_1 semantic presentation

begin

definition
let g, s be ( ( real ) ( V30() real ext-real ) number ) ;
:: original: [.
redefine func [.g,s.] -> ( ( ) ( V50() V51() V52() ) Subset of ( ( ) ( ) set ) ) equals :: RCOMP_1:def 1
 { r : ( ( ) ( V30() real ext-real ) Real) where r is ( ( ) ( V30() real ext-real ) Real) : ( g : ( ( Relation-like V6() natural-valued ) ( Relation-like RAT : ( ( ) ( non empty V50() V51() V52() V53() V56() V57() ) set ) -valued V6() complex-valued ext-real-valued real-valued natural-valued ) set ) <= r : ( ( ) ( V30() real ext-real ) Real) & r : ( ( ) ( V30() real ext-real ) Real) <= s : ( ( ) ( ) set ) ) } ;
end;

definition
let g, s be ( ( ext-real ) ( ext-real ) number ) ;
:: original: ].
redefine func ].g,s.[ -> ( ( ) ( V50() V51() V52() ) Subset of ( ( ) ( ) set ) ) equals :: RCOMP_1:def 2
 { r : ( ( ) ( V30() real ext-real ) Real) where r is ( ( ) ( V30() real ext-real ) Real) : ( g : ( ( Relation-like V6() natural-valued ) ( Relation-like RAT : ( ( ) ( non empty V50() V51() V52() V53() V56() V57() ) set ) -valued V6() complex-valued ext-real-valued real-valued natural-valued ) set ) < r : ( ( ) ( V30() real ext-real ) Real) & r : ( ( ) ( V30() real ext-real ) Real) < s : ( ( ) ( ) set ) ) } ;
end;

theorem :: RCOMP_1:1
for r, p, g being ( ( real ) ( V30() real ext-real ) number ) holds
( r : ( ( real ) ( V30() real ext-real ) number ) in ].(p : ( ( real ) ( V30() real ext-real ) number ) - g : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) set ) ,(p : ( ( real ) ( V30() real ext-real ) number ) + g : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) set ) .[ : ( ( ) ( V50() V51() V52() non left_end non right_end V71() ) Subset of ( ( ) ( ) set ) ) iff abs (r : ( ( real ) ( V30() real ext-real ) number ) - p : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) set ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) < g : ( ( real ) ( V30() real ext-real ) number ) ) ;

theorem :: RCOMP_1:2
for r, p, g being ( ( real ) ( V30() real ext-real ) number ) holds
( r : ( ( real ) ( V30() real ext-real ) number ) in [.p : ( ( real ) ( V30() real ext-real ) number ) ,g : ( ( real ) ( V30() real ext-real ) number ) .] : ( ( ) ( V50() V51() V52() V71() ) Subset of ( ( ) ( ) set ) ) iff abs ((p : ( ( real ) ( V30() real ext-real ) number ) + g : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) set ) - (2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative V48() V49() V50() V51() V52() V53() V54() V55() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) ) * r : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) <= g : ( ( real ) ( V30() real ext-real ) number ) - p : ( ( real ) ( V30() real ext-real ) number ) : ( ( ) ( V30() real ext-real ) set ) ) ;

theorem :: RCOMP_1:3
for r, p, g being ( ( real ) ( V30() real ext-real ) number ) holds
( r : ( ( real ) ( V30() real ext-real ) number ) in ].p : ( ( real ) ( V30() real ext-real ) number ) ,g : ( ( real ) ( V30() real ext-real ) number ) .[ : ( ( ) ( V50() V51() V52() non left_end non right_end V71() ) Subset of ( ( ) ( ) set ) ) iff abs ((p : ( ( real ) ( V30() real ext-real ) number ) + g : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) set ) - (2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative V48() V49() V50() V51() V52() V53() V54() V55() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) ) * r : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) < g : ( ( real ) ( V30() real ext-real ) number ) - p : ( ( real ) ( V30() real ext-real ) number ) : ( ( ) ( V30() real ext-real ) set ) ) ;

definition
let X be ( ( ) ( V50() V51() V52() ) Subset of ( ( ) ( ) set ) ) ;
attr X is compact means :: RCOMP_1:def 3
 for s1 being ( ( V6() V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) -valued V6() non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) complex-valued ext-real-valued real-valued ) Real_Sequence) st rng s1 : ( ( V6() V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) -valued V6() non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) complex-valued ext-real-valued real-valued ) Real_Sequence) : ( ( ) ( V50() V51() V52() ) set ) c= X : ( ( Relation-like V6() natural-valued ) ( Relation-like RAT : ( ( ) ( non empty V50() V51() V52() V53() V56() V57() ) set ) -valued V6() complex-valued ext-real-valued real-valued natural-valued ) set ) holds
ex s2 being ( ( V6() V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) -valued V6() non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) complex-valued ext-real-valued real-valued ) Real_Sequence) st
( s2 : ( ( V6() V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) -valued V6() non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) complex-valued ext-real-valued real-valued ) Real_Sequence) is ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) -valued V6() non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) complex-valued ext-real-valued real-valued ) subsequence of s1 : ( ( V6() V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) -valued V6() non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) complex-valued ext-real-valued real-valued ) Real_Sequence) ) & s2 : ( ( V6() V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) -valued V6() non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) complex-valued ext-real-valued real-valued ) Real_Sequence) is convergent & lim s2 : ( ( V6() V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) -valued V6() non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) complex-valued ext-real-valued real-valued ) Real_Sequence) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) in X : ( ( Relation-like V6() natural-valued ) ( Relation-like RAT : ( ( ) ( non empty V50() V51() V52() V53() V56() V57() ) set ) -valued V6() complex-valued ext-real-valued real-valued natural-valued ) set ) );
end;

definition
let X be ( ( ) ( V50() V51() V52() ) Subset of ( ( ) ( ) set ) ) ;
attr X is closed means :: RCOMP_1:def 4
 for s1 being ( ( V6() V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) -valued V6() non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) complex-valued ext-real-valued real-valued ) Real_Sequence) st rng s1 : ( ( V6() V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) -valued V6() non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) complex-valued ext-real-valued real-valued ) Real_Sequence) : ( ( ) ( V50() V51() V52() ) set ) c= X : ( ( Relation-like V6() natural-valued ) ( Relation-like RAT : ( ( ) ( non empty V50() V51() V52() V53() V56() V57() ) set ) -valued V6() complex-valued ext-real-valued real-valued natural-valued ) set ) & s1 : ( ( V6() V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) -valued V6() non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) complex-valued ext-real-valued real-valued ) Real_Sequence) is convergent holds
lim s1 : ( ( V6() V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) -valued V6() non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) complex-valued ext-real-valued real-valued ) Real_Sequence) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) in X : ( ( Relation-like V6() natural-valued ) ( Relation-like RAT : ( ( ) ( non empty V50() V51() V52() V53() V56() V57() ) set ) -valued V6() complex-valued ext-real-valued real-valued natural-valued ) set ) ;
end;

definition
let X be ( ( ) ( V50() V51() V52() ) Subset of ( ( ) ( ) set ) ) ;
attr X is open means :: RCOMP_1:def 5
X : ( ( Relation-like V6() natural-valued ) ( Relation-like RAT : ( ( ) ( non empty V50() V51() V52() V53() V56() V57() ) set ) -valued V6() complex-valued ext-real-valued real-valued natural-valued ) set ) ` : ( ( ) ( V50() V51() V52() ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) is closed ;
end;

theorem :: RCOMP_1:4
for s, g being ( ( real ) ( V30() real ext-real ) number )
for s1 being ( ( V6() V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) -valued V6() non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) complex-valued ext-real-valued real-valued ) Real_Sequence) st rng s1 : ( ( V6() V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) -valued V6() non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) complex-valued ext-real-valued real-valued ) Real_Sequence) : ( ( ) ( V50() V51() V52() ) set ) c= [.s : ( ( real ) ( V30() real ext-real ) number ) ,g : ( ( real ) ( V30() real ext-real ) number ) .] : ( ( ) ( V50() V51() V52() V71() ) Subset of ( ( ) ( ) set ) ) holds
s1 : ( ( V6() V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) -valued V6() non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) complex-valued ext-real-valued real-valued ) Real_Sequence) is bounded ;

theorem :: RCOMP_1:5
for s, g being ( ( real ) ( V30() real ext-real ) number ) holds [.s : ( ( real ) ( V30() real ext-real ) number ) ,g : ( ( real ) ( V30() real ext-real ) number ) .] : ( ( ) ( V50() V51() V52() V71() ) Subset of ( ( ) ( ) set ) ) is closed ;

theorem :: RCOMP_1:6
for s, g being ( ( real ) ( V30() real ext-real ) number ) holds [.s : ( ( real ) ( V30() real ext-real ) number ) ,g : ( ( real ) ( V30() real ext-real ) number ) .] : ( ( ) ( V50() V51() V52() V71() ) Subset of ( ( ) ( ) set ) ) is compact ;

theorem :: RCOMP_1:7
for p, q being ( ( real ) ( V30() real ext-real ) number ) holds ].p : ( ( real ) ( V30() real ext-real ) number ) ,q : ( ( real ) ( V30() real ext-real ) number ) .[ : ( ( ) ( V50() V51() V52() non left_end non right_end V71() ) Subset of ( ( ) ( ) set ) ) is open ;

registration
let p, q be ( ( real ) ( V30() real ext-real ) number ) ;
cluster ].p : ( ( real ) ( V30() real ext-real ) set ) ,q : ( ( real ) ( V30() real ext-real ) set ) .[ : ( ( ) ( non left_end non right_end V71() ) set ) -> open for ( ( ) ( V50() V51() V52() ) Subset of ( ( ) ( ) set ) ) ;
cluster [.p : ( ( real ) ( V30() real ext-real ) set ) ,q : ( ( real ) ( V30() real ext-real ) set ) .] : ( ( ) ( V71() ) set ) -> closed for ( ( ) ( V50() V51() V52() ) Subset of ( ( ) ( ) set ) ) ;
end;

theorem :: RCOMP_1:8
for X being ( ( ) ( V50() V51() V52() ) Subset of ( ( ) ( ) set ) ) st X : ( ( ) ( V50() V51() V52() ) Subset of ( ( ) ( ) set ) ) is compact holds
X : ( ( ) ( V50() V51() V52() ) Subset of ( ( ) ( ) set ) ) is closed ;

registration
cluster compact -> closed for ( ( ) ( ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) ;
end;

theorem :: RCOMP_1:9
for s1 being ( ( V6() V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) -valued V6() non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) complex-valued ext-real-valued real-valued ) Real_Sequence)
for X being ( ( ) ( V50() V51() V52() ) Subset of ( ( ) ( ) set ) ) st ( for p being ( ( real ) ( V30() real ext-real ) number ) st p : ( ( V6() V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) -valued V6() non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) complex-valued ext-real-valued real-valued ) Real_Sequence) in X : ( ( ) ( V50() V51() V52() ) Subset of ( ( ) ( ) set ) ) holds
ex r being ( ( real ) ( V30() real ext-real ) number ) ex n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) ) st
( 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) ) < r : ( ( real ) ( V30() real ext-real ) number ) & ( for m being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) ) st n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) ) < m : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) ) holds
r : ( ( real ) ( V30() real ext-real ) number ) < abs ((s1 : ( ( V6() V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) -valued V6() non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) complex-valued ext-real-valued real-valued ) Real_Sequence) . m : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) - p : ( ( V6() V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) -valued V6() non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) complex-valued ext-real-valued real-valued ) Real_Sequence) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) ) ) ) holds
for s2 being ( ( V6() V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) -valued V6() non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) complex-valued ext-real-valued real-valued ) Real_Sequence) st s2 : ( ( V6() V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) -valued V6() non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) complex-valued ext-real-valued real-valued ) Real_Sequence) is ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) -valued V6() non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) complex-valued ext-real-valued real-valued ) subsequence of s1 : ( ( V6() V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) -valued V6() non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) complex-valued ext-real-valued real-valued ) Real_Sequence) ) & s2 : ( ( V6() V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) -valued V6() non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) complex-valued ext-real-valued real-valued ) Real_Sequence) is convergent holds
not lim s2 : ( ( V6() V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) -valued V6() non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) complex-valued ext-real-valued real-valued ) Real_Sequence) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) in X : ( ( ) ( V50() V51() V52() ) Subset of ( ( ) ( ) set ) ) ;

theorem :: RCOMP_1:10
for X being ( ( ) ( V50() V51() V52() ) Subset of ( ( ) ( ) set ) ) st X : ( ( ) ( V50() V51() V52() ) Subset of ( ( ) ( ) set ) ) is compact holds
X : ( ( ) ( V50() V51() V52() ) Subset of ( ( ) ( ) set ) ) is real-bounded ;

theorem :: RCOMP_1:11
for X being ( ( ) ( V50() V51() V52() ) Subset of ( ( ) ( ) set ) ) st X : ( ( ) ( V50() V51() V52() ) Subset of ( ( ) ( ) set ) ) is real-bounded & X : ( ( ) ( V50() V51() V52() ) Subset of ( ( ) ( ) set ) ) is closed holds
X : ( ( ) ( V50() V51() V52() ) Subset of ( ( ) ( ) set ) ) is compact ;

theorem :: RCOMP_1:12
for X being ( ( ) ( V50() V51() V52() ) Subset of ( ( ) ( ) set ) ) st X : ( ( ) ( V50() V51() V52() ) Subset of ( ( ) ( ) set ) ) <> {} : ( ( ) ( ) set ) & X : ( ( ) ( V50() V51() V52() ) Subset of ( ( ) ( ) set ) ) is closed & X : ( ( ) ( V50() V51() V52() ) Subset of ( ( ) ( ) set ) ) is bounded_above holds
upper_bound X : ( ( ) ( V50() V51() V52() ) Subset of ( ( ) ( ) set ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) in X : ( ( ) ( V50() V51() V52() ) Subset of ( ( ) ( ) set ) ) ;

theorem :: RCOMP_1:13
for X being ( ( ) ( V50() V51() V52() ) Subset of ( ( ) ( ) set ) ) st X : ( ( ) ( V50() V51() V52() ) Subset of ( ( ) ( ) set ) ) <> {} : ( ( ) ( ) set ) & X : ( ( ) ( V50() V51() V52() ) Subset of ( ( ) ( ) set ) ) is closed & X : ( ( ) ( V50() V51() V52() ) Subset of ( ( ) ( ) set ) ) is bounded_below holds
lower_bound X : ( ( ) ( V50() V51() V52() ) Subset of ( ( ) ( ) set ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) in X : ( ( ) ( V50() V51() V52() ) Subset of ( ( ) ( ) set ) ) ;

theorem :: RCOMP_1:14
for X being ( ( ) ( V50() V51() V52() ) Subset of ( ( ) ( ) set ) ) st X : ( ( ) ( V50() V51() V52() ) Subset of ( ( ) ( ) set ) ) <> {} : ( ( ) ( ) set ) & X : ( ( ) ( V50() V51() V52() ) Subset of ( ( ) ( ) set ) ) is compact holds
( upper_bound X : ( ( ) ( V50() V51() V52() ) Subset of ( ( ) ( ) set ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) in X : ( ( ) ( V50() V51() V52() ) Subset of ( ( ) ( ) set ) ) & lower_bound X : ( ( ) ( V50() V51() V52() ) Subset of ( ( ) ( ) set ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) in X : ( ( ) ( V50() V51() V52() ) Subset of ( ( ) ( ) set ) ) ) ;

theorem :: RCOMP_1:15
for X being ( ( ) ( V50() V51() V52() ) Subset of ( ( ) ( ) set ) ) st X : ( ( ) ( V50() V51() V52() ) Subset of ( ( ) ( ) set ) ) is compact & ( for g1, g2 being ( ( real ) ( V30() real ext-real ) number ) st g1 : ( ( real ) ( V30() real ext-real ) number ) in X : ( ( ) ( V50() V51() V52() ) Subset of ( ( ) ( ) set ) ) & g2 : ( ( real ) ( V30() real ext-real ) number ) in X : ( ( ) ( V50() V51() V52() ) Subset of ( ( ) ( ) set ) ) holds
[.g1 : ( ( real ) ( V30() real ext-real ) number ) ,g2 : ( ( real ) ( V30() real ext-real ) number ) .] : ( ( ) ( V50() V51() V52() V71() closed ) Subset of ( ( ) ( ) set ) ) c= X : ( ( ) ( V50() V51() V52() ) Subset of ( ( ) ( ) set ) ) ) holds
ex p, g being ( ( real ) ( V30() real ext-real ) number ) st X : ( ( ) ( V50() V51() V52() ) Subset of ( ( ) ( ) set ) ) = [.p : ( ( real ) ( V30() real ext-real ) number ) ,g : ( ( real ) ( V30() real ext-real ) number ) .] : ( ( ) ( V50() V51() V52() V71() closed ) Subset of ( ( ) ( ) set ) ) ;

registration
cluster V50() V51() V52() open for ( ( ) ( ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) ;
end;

definition
let r be ( ( real ) ( V30() real ext-real ) number ) ;
mode Neighbourhood of r -> ( ( ) ( V50() V51() V52() ) Subset of ( ( ) ( ) set ) ) means :: RCOMP_1:def 6
 ex g being ( ( real ) ( V30() real ext-real ) number ) st
( 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) ) < g : ( ( real ) ( V30() real ext-real ) number ) & it : ( ( ) ( ) set ) = ].(r : ( ( ) ( ) set ) - g : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( ) set ) ,(r : ( ( ) ( ) set ) + g : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( ) set ) .[ : ( ( ) ( V50() V51() V52() ) Subset of ( ( ) ( ) set ) ) );
end;

registration
let r be ( ( real ) ( V30() real ext-real ) number ) ;
cluster -> open for ( ( ) ( ) Neighbourhood of r : ( ( ) ( ) set ) ) ;
end;

theorem :: RCOMP_1:16
for r being ( ( real ) ( V30() real ext-real ) number )
for N being ( ( ) ( V50() V51() V52() open ) Neighbourhood of r : ( ( real ) ( V30() real ext-real ) number ) ) holds r : ( ( real ) ( V30() real ext-real ) number ) in N : ( ( ) ( V50() V51() V52() open ) Neighbourhood of b1 : ( ( real ) ( V30() real ext-real ) number ) ) ;

theorem :: RCOMP_1:17
for r being ( ( real ) ( V30() real ext-real ) number )
for N1, N2 being ( ( ) ( V50() V51() V52() open ) Neighbourhood of r : ( ( real ) ( V30() real ext-real ) number ) ) ex N being ( ( ) ( V50() V51() V52() open ) Neighbourhood of r : ( ( real ) ( V30() real ext-real ) number ) ) st
( N : ( ( ) ( V50() V51() V52() open ) Neighbourhood of b1 : ( ( real ) ( V30() real ext-real ) number ) ) c= N1 : ( ( ) ( V50() V51() V52() open ) Neighbourhood of b1 : ( ( real ) ( V30() real ext-real ) number ) ) & N : ( ( ) ( V50() V51() V52() open ) Neighbourhood of b1 : ( ( real ) ( V30() real ext-real ) number ) ) c= N2 : ( ( ) ( V50() V51() V52() open ) Neighbourhood of b1 : ( ( real ) ( V30() real ext-real ) number ) ) ) ;

theorem :: RCOMP_1:18
for X being ( ( open ) ( V50() V51() V52() open ) Subset of ( ( ) ( ) set ) )
for r being ( ( real ) ( V30() real ext-real ) number ) st r : ( ( real ) ( V30() real ext-real ) number ) in X : ( ( open ) ( V50() V51() V52() open ) Subset of ( ( ) ( ) set ) ) holds
ex N being ( ( ) ( V50() V51() V52() open ) Neighbourhood of r : ( ( real ) ( V30() real ext-real ) number ) ) st N : ( ( ) ( V50() V51() V52() open ) Neighbourhood of b2 : ( ( real ) ( V30() real ext-real ) number ) ) c= X : ( ( open ) ( V50() V51() V52() open ) Subset of ( ( ) ( ) set ) ) ;

theorem :: RCOMP_1:19
for X being ( ( open ) ( V50() V51() V52() open ) Subset of ( ( ) ( ) set ) )
for r being ( ( real ) ( V30() real ext-real ) number ) st r : ( ( real ) ( V30() real ext-real ) number ) in X : ( ( open ) ( V50() V51() V52() open ) Subset of ( ( ) ( ) set ) ) holds
ex g being ( ( real ) ( V30() real ext-real ) number ) st
( 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) : ( ( ) ( ) set ) ) ) < g : ( ( real ) ( V30() real ext-real ) number ) & ].(r : ( ( real ) ( V30() real ext-real ) number ) - g : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) set ) ,(r : ( ( real ) ( V30() real ext-real ) number ) + g : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) set ) .[ : ( ( ) ( V50() V51() V52() non left_end non right_end V71() open ) Subset of ( ( ) ( ) set ) ) c= X : ( ( open ) ( V50() V51() V52() open ) Subset of ( ( ) ( ) set ) ) ) ;

theorem :: RCOMP_1:20
for X being ( ( ) ( V50() V51() V52() ) Subset of ( ( ) ( ) set ) ) st ( for r being ( ( real ) ( V30() real ext-real ) number ) st r : ( ( real ) ( V30() real ext-real ) number ) in X : ( ( ) ( V50() V51() V52() ) Subset of ( ( ) ( ) set ) ) holds
ex N being ( ( ) ( V50() V51() V52() open ) Neighbourhood of r : ( ( real ) ( V30() real ext-real ) number ) ) st N : ( ( ) ( V50() V51() V52() open ) Neighbourhood of b2 : ( ( real ) ( V30() real ext-real ) number ) ) c= X : ( ( ) ( V50() V51() V52() ) Subset of ( ( ) ( ) set ) ) ) holds
X : ( ( ) ( V50() V51() V52() ) Subset of ( ( ) ( ) set ) ) is open ;

theorem :: RCOMP_1:21
for X being ( ( ) ( V50() V51() V52() ) Subset of ( ( ) ( ) set ) ) st X : ( ( ) ( V50() V51() V52() ) Subset of ( ( ) ( ) set ) ) is open & X : ( ( ) ( V50() V51() V52() ) Subset of ( ( ) ( ) set ) ) is bounded_above holds
not upper_bound X : ( ( ) ( V50() V51() V52() ) Subset of ( ( ) ( ) set ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) in X : ( ( ) ( V50() V51() V52() ) Subset of ( ( ) ( ) set ) ) ;

theorem :: RCOMP_1:22
for X being ( ( ) ( V50() V51() V52() ) Subset of ( ( ) ( ) set ) ) st X : ( ( ) ( V50() V51() V52() ) Subset of ( ( ) ( ) set ) ) is open & X : ( ( ) ( V50() V51() V52() ) Subset of ( ( ) ( ) set ) ) is bounded_below holds
not lower_bound X : ( ( ) ( V50() V51() V52() ) Subset of ( ( ) ( ) set ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() ) set ) ) in X : ( ( ) ( V50() V51() V52() ) Subset of ( ( ) ( ) set ) ) ;

theorem :: RCOMP_1:23
for X being ( ( ) ( V50() V51() V52() ) Subset of ( ( ) ( ) set ) ) st X : ( ( ) ( V50() V51() V52() ) Subset of ( ( ) ( ) set ) ) is open & X : ( ( ) ( V50() V51() V52() ) Subset of ( ( ) ( ) set ) ) is real-bounded & ( for g1, g2 being ( ( real ) ( V30() real ext-real ) number ) st g1 : ( ( real ) ( V30() real ext-real ) number ) in X : ( ( ) ( V50() V51() V52() ) Subset of ( ( ) ( ) set ) ) & g2 : ( ( real ) ( V30() real ext-real ) number ) in X : ( ( ) ( V50() V51() V52() ) Subset of ( ( ) ( ) set ) ) holds
[.g1 : ( ( real ) ( V30() real ext-real ) number ) ,g2 : ( ( real ) ( V30() real ext-real ) number ) .] : ( ( ) ( V50() V51() V52() V71() closed ) Subset of ( ( ) ( ) set ) ) c= X : ( ( ) ( V50() V51() V52() ) Subset of ( ( ) ( ) set ) ) ) holds
ex p, g being ( ( real ) ( V30() real ext-real ) number ) st X : ( ( ) ( V50() V51() V52() ) Subset of ( ( ) ( ) set ) ) = ].p : ( ( real ) ( V30() real ext-real ) number ) ,g : ( ( real ) ( V30() real ext-real ) number ) .[ : ( ( ) ( V50() V51() V52() non left_end non right_end V71() open ) Subset of ( ( ) ( ) set ) ) ;

definition
let g be ( ( real ) ( V30() real ext-real ) number ) ;
let s be ( ( ext-real ) ( ext-real ) number ) ;
:: original: [.
redefine func [.g,s.[ -> ( ( ) ( V50() V51() V52() ) Subset of ( ( ) ( ) set ) ) equals :: RCOMP_1:def 7
 { r : ( ( ) ( V30() real ext-real ) Real) where r is ( ( ) ( V30() real ext-real ) Real) : ( g : ( ( ) ( ) set ) <= r : ( ( ) ( V30() real ext-real ) Real) & r : ( ( ) ( V30() real ext-real ) Real) < s : ( ( ) ( ) set ) ) } ;
end;

definition
let g be ( ( ext-real ) ( ext-real ) number ) ;
let s be ( ( real ) ( V30() real ext-real ) number ) ;
:: original: ].
redefine func ].g,s.] -> ( ( ) ( V50() V51() V52() ) Subset of ( ( ) ( ) set ) ) equals :: RCOMP_1:def 8
 { r : ( ( ) ( V30() real ext-real ) Real) where r is ( ( ) ( V30() real ext-real ) Real) : ( g : ( ( ) ( ) set ) < r : ( ( ) ( V30() real ext-real ) Real) & r : ( ( ) ( V30() real ext-real ) Real) <= s : ( ( ) ( ) set ) ) } ;
end;