:: KURATO_0 semantic presentation

begin

theorem :: KURATO_0:1
for F being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function)
for i being ( ( ) ( ) set ) st i : ( ( ) ( ) set ) in dom F : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) holds
meet F : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) c= F : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) . i : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

theorem :: KURATO_0:2
for A, B, C, D being ( ( ) ( ) set ) st A : ( ( ) ( ) set ) meets B : ( ( ) ( ) set ) & C : ( ( ) ( ) set ) meets D : ( ( ) ( ) set ) holds
[:A : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) meets [:B : ( ( ) ( ) set ) ,D : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) ;

registration
let X be ( ( ) ( ) set ) ;
cluster Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool X : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) : ( ( ) ( non empty ) Element of bool (bool X : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) -> non empty Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool X : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) : ( ( ) ( non empty ) Element of bool (bool X : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) for ( ( ) ( ) Element of bool [:NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,(bool X : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) ) : ( ( ) ( non empty ) Element of bool (bool X : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ;
end;

registration
let T be ( ( non empty ) ( non empty ) set ) ;
cluster non empty Relation-like non-empty NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool T : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool T : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool T : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool T : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) for ( ( ) ( ) Element of bool [:NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,(bool T : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool T : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ;
end;

definition
let X be ( ( ) ( ) set ) ;
let F be ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool X : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool X : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool X : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ;
:: original: Union
redefine func Union F -> ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;
:: original: meet
redefine func meet F -> ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;
end;

begin

definition
let X be ( ( ) ( ) set ) ;
let F be ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool X : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool X : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool X : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ;
func lim_inf F -> ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) means :: KURATO_0:def 1
 ex f being ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool X : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool X : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool X : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool X : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool X : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool X : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool X : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) st
( it : ( ( ) ( ) Element of bool (bool X : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) = Union f : ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool X : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool X : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool X : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) & ( for n being ( ( ) ( V7() V8() V9() V13() V14() V15() ext-real non negative ) Element of NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) holds f : ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool X : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool X : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool X : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) . n : ( ( ) ( V7() V8() V9() V13() V14() V15() ext-real non negative ) Element of NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool X : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool X : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) = meet (F : ( ( ) ( ) set ) ^\ n : ( ( ) ( V7() V8() V9() V13() V14() V15() ext-real non negative ) Element of NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool X : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool X : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool X : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool X : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool X : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool X : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) Element of bool [:NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,(bool X : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool X : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) );
func lim_sup F -> ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) means :: KURATO_0:def 2
 ex f being ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool X : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool X : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool X : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool X : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool X : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool X : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool X : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) st
( it : ( ( ) ( ) Element of bool (bool X : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) = meet f : ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool X : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool X : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool X : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) & ( for n being ( ( ) ( V7() V8() V9() V13() V14() V15() ext-real non negative ) Element of NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) holds f : ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool X : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool X : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool X : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) . n : ( ( ) ( V7() V8() V9() V13() V14() V15() ext-real non negative ) Element of NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool X : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool X : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) = Union (F : ( ( ) ( ) set ) ^\ n : ( ( ) ( V7() V8() V9() V13() V14() V15() ext-real non negative ) Element of NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool X : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool X : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool X : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool X : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool X : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool X : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) Element of bool [:NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,(bool X : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool X : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) );
end;

theorem :: KURATO_0:3
for X being ( ( ) ( ) set )
for F being ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) )
for x being ( ( ) ( ) set ) holds
( x : ( ( ) ( ) set ) in meet F : ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) iff for z being ( ( ) ( V7() V8() V9() V13() V14() V15() ext-real non negative ) Element of NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) holds x : ( ( ) ( ) set ) in F : ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) . z : ( ( ) ( V7() V8() V9() V13() V14() V15() ext-real non negative ) Element of NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ;

theorem :: KURATO_0:4
for X being ( ( ) ( ) set )
for F being ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) )
for x being ( ( ) ( ) set ) holds
( x : ( ( ) ( ) set ) in lim_inf F : ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) iff ex n being ( ( ) ( V7() V8() V9() V13() V14() V15() ext-real non negative ) Element of NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) st
for k being ( ( ) ( V7() V8() V9() V13() V14() V15() ext-real non negative ) Element of NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) holds x : ( ( ) ( ) set ) in F : ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) . (n : ( ( ) ( V7() V8() V9() V13() V14() V15() ext-real non negative ) Element of NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) + k : ( ( ) ( V7() V8() V9() V13() V14() V15() ext-real non negative ) Element of NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V7() V8() V9() V13() V14() V15() ext-real non negative ) Element of NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ;

theorem :: KURATO_0:5
for X being ( ( ) ( ) set )
for F being ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) )
for x being ( ( ) ( ) set ) holds
( x : ( ( ) ( ) set ) in lim_sup F : ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) iff for n being ( ( ) ( V7() V8() V9() V13() V14() V15() ext-real non negative ) Element of NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ex k being ( ( ) ( V7() V8() V9() V13() V14() V15() ext-real non negative ) Element of NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) st x : ( ( ) ( ) set ) in F : ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) . (n : ( ( ) ( V7() V8() V9() V13() V14() V15() ext-real non negative ) Element of NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) + k : ( ( ) ( V7() V8() V9() V13() V14() V15() ext-real non negative ) Element of NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V7() V8() V9() V13() V14() V15() ext-real non negative ) Element of NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ;

theorem :: KURATO_0:6
for X being ( ( ) ( ) set )
for F being ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) holds lim_inf F : ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) c= lim_sup F : ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: KURATO_0:7
for X being ( ( ) ( ) set )
for F being ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) holds meet F : ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) c= lim_inf F : ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: KURATO_0:8
for X being ( ( ) ( ) set )
for F being ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) holds lim_sup F : ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) c= Union F : ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: KURATO_0:9
for X being ( ( ) ( ) set )
for F being ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) holds lim_inf F : ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) = (lim_sup (Complement F : ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) Element of bool [:NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,(bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ` : ( ( ) ( ) Element of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: KURATO_0:10
for X being ( ( ) ( ) set )
for A, B, C being ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) st ( for n being ( ( ) ( V7() V8() V9() V13() V14() V15() ext-real non negative ) Element of NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) holds C : ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) . n : ( ( ) ( V7() V8() V9() V13() V14() V15() ext-real non negative ) Element of NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) = (A : ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) . n : ( ( ) ( V7() V8() V9() V13() V14() V15() ext-real non negative ) Element of NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) /\ (B : ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) . n : ( ( ) ( V7() V8() V9() V13() V14() V15() ext-real non negative ) Element of NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) holds
lim_inf C : ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) = (lim_inf A : ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) /\ (lim_inf B : ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: KURATO_0:11
for X being ( ( ) ( ) set )
for A, B, C being ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) st ( for n being ( ( ) ( V7() V8() V9() V13() V14() V15() ext-real non negative ) Element of NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) holds C : ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) . n : ( ( ) ( V7() V8() V9() V13() V14() V15() ext-real non negative ) Element of NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) = (A : ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) . n : ( ( ) ( V7() V8() V9() V13() V14() V15() ext-real non negative ) Element of NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) \/ (B : ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) . n : ( ( ) ( V7() V8() V9() V13() V14() V15() ext-real non negative ) Element of NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) holds
lim_sup C : ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) = (lim_sup A : ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) \/ (lim_sup B : ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: KURATO_0:12
for X being ( ( ) ( ) set )
for A, B, C being ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) st ( for n being ( ( ) ( V7() V8() V9() V13() V14() V15() ext-real non negative ) Element of NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) holds C : ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) . n : ( ( ) ( V7() V8() V9() V13() V14() V15() ext-real non negative ) Element of NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) = (A : ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) . n : ( ( ) ( V7() V8() V9() V13() V14() V15() ext-real non negative ) Element of NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) \/ (B : ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) . n : ( ( ) ( V7() V8() V9() V13() V14() V15() ext-real non negative ) Element of NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) holds
(lim_inf A : ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) \/ (lim_inf B : ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) c= lim_inf C : ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: KURATO_0:13
for X being ( ( ) ( ) set )
for A, B, C being ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) st ( for n being ( ( ) ( V7() V8() V9() V13() V14() V15() ext-real non negative ) Element of NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) holds C : ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) . n : ( ( ) ( V7() V8() V9() V13() V14() V15() ext-real non negative ) Element of NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) = (A : ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) . n : ( ( ) ( V7() V8() V9() V13() V14() V15() ext-real non negative ) Element of NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) /\ (B : ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) . n : ( ( ) ( V7() V8() V9() V13() V14() V15() ext-real non negative ) Element of NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) holds
lim_sup C : ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) c= (lim_sup A : ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) /\ (lim_sup B : ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: KURATO_0:14
for X being ( ( ) ( ) set )
for A being ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) )
for B being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) st ( for n being ( ( V13() ) ( V7() V8() V9() V13() V14() V15() ext-real non negative ) Nat) holds A : ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) . n : ( ( V13() ) ( V7() V8() V9() V13() V14() V15() ext-real non negative ) Nat) : ( ( ) ( ) set ) = B : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) holds
lim_sup A : ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) = B : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: KURATO_0:15
for X being ( ( ) ( ) set )
for A being ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) )
for B being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) st ( for n being ( ( V13() ) ( V7() V8() V9() V13() V14() V15() ext-real non negative ) Nat) holds A : ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) . n : ( ( V13() ) ( V7() V8() V9() V13() V14() V15() ext-real non negative ) Nat) : ( ( ) ( ) set ) = B : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) holds
lim_inf A : ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) = B : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: KURATO_0:16
for X being ( ( ) ( ) set )
for A, B being ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) )
for C being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) st ( for n being ( ( ) ( V7() V8() V9() V13() V14() V15() ext-real non negative ) Element of NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) holds B : ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) . n : ( ( ) ( V7() V8() V9() V13() V14() V15() ext-real non negative ) Element of NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) = C : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) \+\ (A : ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) . n : ( ( ) ( V7() V8() V9() V13() V14() V15() ext-real non negative ) Element of NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) holds
C : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) \+\ (lim_inf A : ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) c= lim_sup B : ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: KURATO_0:17
for X being ( ( ) ( ) set )
for A, B being ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) )
for C being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) st ( for n being ( ( ) ( V7() V8() V9() V13() V14() V15() ext-real non negative ) Element of NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) holds B : ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) . n : ( ( ) ( V7() V8() V9() V13() V14() V15() ext-real non negative ) Element of NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) = C : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) \+\ (A : ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) . n : ( ( ) ( V7() V8() V9() V13() V14() V15() ext-real non negative ) Element of NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) holds
C : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) \+\ (lim_sup A : ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) c= lim_sup B : ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;

begin

theorem :: KURATO_0:18
for f being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) st ( for i being ( ( ) ( V7() V8() V9() V13() V14() V15() ext-real non negative ) Element of NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) holds f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) . (i : ( ( ) ( V7() V8() V9() V13() V14() V15() ext-real non negative ) Element of NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty V7() V8() V9() V13() V14() V15() ext-real positive non negative ) Element of NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty V7() V8() V9() V13() V14() V15() ext-real positive non negative ) Element of NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) c= f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) . i : ( ( ) ( V7() V8() V9() V13() V14() V15() ext-real non negative ) Element of NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ) holds
for i, j being ( ( ) ( V7() V8() V9() V13() V14() V15() ext-real non negative ) Element of NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) st i : ( ( ) ( V7() V8() V9() V13() V14() V15() ext-real non negative ) Element of NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) <= j : ( ( ) ( V7() V8() V9() V13() V14() V15() ext-real non negative ) Element of NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) holds
f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) . j : ( ( ) ( V7() V8() V9() V13() V14() V15() ext-real non negative ) Element of NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) c= f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) . i : ( ( ) ( V7() V8() V9() V13() V14() V15() ext-real non negative ) Element of NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ;

definition
let T be ( ( ) ( ) set ) ;
let S be ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool T : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool T : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool T : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool T : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool T : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool T : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool T : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ;
:: original: non-ascending
redefine attr S is non-ascending means :: KURATO_0:def 3
 for i being ( ( ) ( V7() V8() V9() V13() V14() V15() ext-real non negative ) Element of NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) holds S : ( ( ) ( ) set ) . (i : ( ( ) ( V7() V8() V9() V13() V14() V15() ext-real non negative ) Element of NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty V7() V8() V9() V13() V14() V15() ext-real positive non negative ) Element of NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty V7() V8() V9() V13() V14() V15() ext-real positive non negative ) Element of NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool T : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool T : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) c= S : ( ( ) ( ) set ) . i : ( ( ) ( V7() V8() V9() V13() V14() V15() ext-real non negative ) Element of NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool T : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool T : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ;
:: original: non-descending
redefine attr S is non-descending means :: KURATO_0:def 4
 for i being ( ( ) ( V7() V8() V9() V13() V14() V15() ext-real non negative ) Element of NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) holds S : ( ( ) ( ) set ) . i : ( ( ) ( V7() V8() V9() V13() V14() V15() ext-real non negative ) Element of NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool T : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool T : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) c= S : ( ( ) ( ) set ) . (i : ( ( ) ( V7() V8() V9() V13() V14() V15() ext-real non negative ) Element of NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty V7() V8() V9() V13() V14() V15() ext-real positive non negative ) Element of NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty V7() V8() V9() V13() V14() V15() ext-real positive non negative ) Element of NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool T : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool T : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ;
end;

theorem :: KURATO_0:19
for T being ( ( ) ( ) set )
for F being ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool T : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) )
for x being ( ( ) ( ) set ) st F : ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) is V50() & ex k being ( ( ) ( V7() V8() V9() V13() V14() V15() ext-real non negative ) Element of NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) st
for n being ( ( ) ( V7() V8() V9() V13() V14() V15() ext-real non negative ) Element of NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) st n : ( ( ) ( V7() V8() V9() V13() V14() V15() ext-real non negative ) Element of NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) > k : ( ( ) ( V7() V8() V9() V13() V14() V15() ext-real non negative ) Element of NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) holds
x : ( ( ) ( ) set ) in F : ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) . n : ( ( ) ( V7() V8() V9() V13() V14() V15() ext-real non negative ) Element of NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) holds
x : ( ( ) ( ) set ) in meet F : ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: KURATO_0:20
for T being ( ( ) ( ) set )
for F being ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool T : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) st F : ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) is V50() holds
lim_inf F : ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) = meet F : ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: KURATO_0:21
for T being ( ( ) ( ) set )
for F being ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool T : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) st F : ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) is V51() holds
lim_sup F : ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) = Union F : ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;

begin

definition
let T be ( ( ) ( ) set ) ;
let S be ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool T : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool T : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool T : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool T : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool T : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool T : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool T : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ;
attr S is convergent means :: KURATO_0:def 5
 lim_sup S : ( ( ) ( ) set ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) = lim_inf S : ( ( ) ( ) set ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;
end;

theorem :: KURATO_0:22
for T being ( ( ) ( ) set )
for S being ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool T : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) st S : ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) is constant holds
the_value_of S : ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) is ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;

registration
let T be ( ( ) ( ) set ) ;
cluster Function-like constant V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool T : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool T : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) -> Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool T : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool T : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V50() V51() convergent for ( ( ) ( ) Element of bool [:NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,(bool T : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool T : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ;
end;

registration
let T be ( ( ) ( ) set ) ;
cluster non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool T : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool T : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like constant V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool T : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool T : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) for ( ( ) ( ) Element of bool [:NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,(bool T : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) Element of bool (bool T : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ;
end;

notation
let T be ( ( ) ( ) set ) ;
let S be ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool T : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool T : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) convergent ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool T : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool T : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool T : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool T : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) convergent ) SetSequence of ( ( ) ( non empty ) Element of bool (bool T : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ;
synonym Lim_K S for lim_sup S;
end;

theorem :: KURATO_0:23
for X being ( ( ) ( ) set )
for F being ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) convergent ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) convergent ) SetSequence of ( ( ) ( non empty ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) )
for x being ( ( ) ( ) set ) holds
( x : ( ( ) ( ) set ) in Lim_K F : ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) convergent ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) convergent ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) iff ex n being ( ( ) ( V7() V8() V9() V13() V14() V15() ext-real non negative ) Element of NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) st
for k being ( ( ) ( V7() V8() V9() V13() V14() V15() ext-real non negative ) Element of NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) holds x : ( ( ) ( ) set ) in F : ( ( Function-like V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) convergent ) ( non empty Relation-like NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V29( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) V33( NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) convergent ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) . (n : ( ( ) ( V7() V8() V9() V13() V14() V15() ext-real non negative ) Element of NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) + k : ( ( ) ( V7() V8() V9() V13() V14() V15() ext-real non negative ) Element of NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V7() V8() V9() V13() V14() V15() ext-real non negative ) Element of NAT : ( ( ) ( non empty V7() V8() V9() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ;