:: CLOSURE1 semantic presentation

begin

scheme :: CLOSURE1:sch 1
MSSUBSET{ F1() -> ( ( ) ( ) set ) , F2() -> ( ( Relation-like V8() F1( ( ( ) ( ) set ) ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V8() F1( ( ( ) ( ) set ) ) : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of F1( ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) , F3() -> ( ( Relation-like F1( ( ( ) ( ) set ) ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like F1( ( ( ) ( ) set ) ) : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of F1( ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) , P1[ ( ( ) ( ) set ) ] } :
( ( for X being ( ( Relation-like F1( ( ( ) ( ) set ) ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like F1( ( ( ) ( ) set ) ) : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of F1( ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) holds
( X : ( ( Relation-like F1( ( ( ) ( ) set ) ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like F1( ( ( ) ( ) set ) ) : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of F1( ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) in F2( ( ( Relation-like V8() F1( ( ( ) ( ) set ) ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V8() F1( ( ( ) ( ) set ) ) : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of F1( ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( Relation-like V8() F1( ( ( ) ( ) set ) ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V8() F1( ( ( ) ( ) set ) ) : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of F1( ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) iff ( X : ( ( Relation-like F1( ( ( ) ( ) set ) ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like F1( ( ( ) ( ) set ) ) : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of F1( ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) in F3( ( ( Relation-like F1( ( ( ) ( ) set ) ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like F1( ( ( ) ( ) set ) ) : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of F1( ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( Relation-like F1( ( ( ) ( ) set ) ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like F1( ( ( ) ( ) set ) ) : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of F1( ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) & P1[X : ( ( Relation-like F1( ( ( ) ( ) set ) ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like F1( ( ( ) ( ) set ) ) : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of F1( ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ] ) ) ) implies F2( ( ( Relation-like V8() F1( ( ( ) ( ) set ) ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V8() F1( ( ( ) ( ) set ) ) : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of F1( ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( Relation-like V8() F1( ( ( ) ( ) set ) ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V8() F1( ( ( ) ( ) set ) ) : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of F1( ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) c= F3( ( ( Relation-like F1( ( ( ) ( ) set ) ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like F1( ( ( ) ( ) set ) ) : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of F1( ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( Relation-like F1( ( ( ) ( ) set ) ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like F1( ( ( ) ( ) set ) ) : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of F1( ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) )
proof end;

theorem :: CLOSURE1:1
for X being ( ( non empty ) ( non empty ) set )
for x, y being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) c= y : ( ( ) ( ) set ) holds
{ t : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) where t is ( ( ) ( ) Element of X : ( ( non empty ) ( non empty ) set ) ) : y : ( ( ) ( ) set ) c= t : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) } c= { z : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) where z is ( ( ) ( ) Element of X : ( ( non empty ) ( non empty ) set ) ) : x : ( ( ) ( ) set ) c= z : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) } ;

theorem :: CLOSURE1:2
for I being ( ( ) ( ) set )
for M being ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) ) st ex A being ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) ) st A : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) in M : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) holds
M : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) is V8() ;

registration
let I be ( ( ) ( ) set ) ;
let F be ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total Function-yielding ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) ManySortedFunction of I : ( ( ) ( ) set ) ) ;
let A be ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) ) ;
cluster F : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total Function-yielding ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) set ) .. A : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) : ( ( Relation-like Function-like ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) -> Relation-like I : ( ( ) ( ) set ) -defined Function-like total for ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like ) Function) ;
end;

definition
let I be ( ( ) ( ) set ) ;
let A, B be ( ( Relation-like V8() I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V8() I : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) ) ;
let F be ( ( ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) ManySortedFunction of A : ( ( Relation-like V8() I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V8() I : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) ) ,B : ( ( Relation-like V8() I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V8() I : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) ) ) ;
let X be ( ( ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) Element of A : ( ( Relation-like V8() I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V8() I : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) ) ) ;
:: original: ..
redefine func F .. X -> ( ( ) ( Relation-like I : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) Element of B : ( ( Relation-like I : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) ( non empty Relation-like I : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) set ) ) ;
end;

theorem :: CLOSURE1:3
for I being ( ( ) ( ) set )
for A, X being ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) )
for B being ( ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) )
for F being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) ManySortedFunction of A : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,B : ( ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) st X : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) in A : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) holds
F : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) ManySortedFunction of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b4 : ( ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) .. X : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) in B : ( ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ;

theorem :: CLOSURE1:4
for I being ( ( ) ( ) set )
for F, G being ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) ManySortedFunction of I : ( ( ) ( ) set ) )
for A being ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) ) st A : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) in doms G : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) ManySortedFunction of b1 : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) holds
F : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) ManySortedFunction of b1 : ( ( ) ( ) set ) ) .. (G : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) ManySortedFunction of b1 : ( ( ) ( ) set ) ) .. A : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) : ( ( Relation-like Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) = (F : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) ManySortedFunction of b1 : ( ( ) ( ) set ) ) ** G : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) ManySortedFunction of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like Function-yielding V25() ) set ) .. A : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) ;

theorem :: CLOSURE1:5
for I being ( ( ) ( ) set )
for F being ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) ManySortedFunction of I : ( ( ) ( ) set ) ) st F : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) ManySortedFunction of b1 : ( ( ) ( ) set ) ) is "1-1" holds
for A, B being ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) ) st A : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) in doms F : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) ManySortedFunction of b1 : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) & B : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) in doms F : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) ManySortedFunction of b1 : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) & F : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) ManySortedFunction of b1 : ( ( ) ( ) set ) ) .. A : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) = F : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) ManySortedFunction of b1 : ( ( ) ( ) set ) ) .. B : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) holds
A : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) = B : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ;

theorem :: CLOSURE1:6
for I being ( ( ) ( ) set )
for F being ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) ManySortedFunction of I : ( ( ) ( ) set ) ) st doms F : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) ManySortedFunction of b1 : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) is V8() & ( for A, B being ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) ) st A : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) in doms F : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) ManySortedFunction of b1 : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) & B : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) in doms F : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) ManySortedFunction of b1 : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) & F : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) ManySortedFunction of b1 : ( ( ) ( ) set ) ) .. A : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) = F : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) ManySortedFunction of b1 : ( ( ) ( ) set ) ) .. B : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) holds
A : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) = B : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) holds
F : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) ManySortedFunction of b1 : ( ( ) ( ) set ) ) is "1-1" ;

theorem :: CLOSURE1:7
for I being ( ( ) ( ) set )
for A, B being ( ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) )
for F, G being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) ManySortedFunction of A : ( ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,B : ( ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) st ( for M being ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) ) st M : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) in A : ( ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) holds
F : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) ManySortedFunction of b2 : ( ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b3 : ( ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) .. M : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) = G : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) ManySortedFunction of b2 : ( ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b3 : ( ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) .. M : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ) holds
F : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) ManySortedFunction of b2 : ( ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b3 : ( ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) = G : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) ManySortedFunction of b2 : ( ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b3 : ( ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) ;

registration
let I be ( ( ) ( ) set ) ;
let M be ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) ) ;
cluster Relation-like V9() I : ( ( ) ( ) set ) -defined Function-like total V42() for ( ( ) ( ) Element of bool M : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty I : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(I : ( ( ) ( ) set ) ,M : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) ) : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) ;
end;

begin

definition
let I be ( ( ) ( ) set ) ;
let M be ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) ) ;
mode MSSetOp of M is ( ( ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) ManySortedFunction of bool M : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty I : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(I : ( ( ) ( ) set ) ,M : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) ) : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) ) , bool M : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty I : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(I : ( ( ) ( ) set ) ,M : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) ) : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) ;
end;

definition
let I be ( ( ) ( ) set ) ;
let M be ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) ) ;
let O be ( ( ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) MSSetOp of M : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) ) ) ;
let X be ( ( ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) Element of bool M : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty I : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(I : ( ( ) ( ) set ) ,M : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) ) ) : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) ;
:: original: ..
redefine func O .. X -> ( ( ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) Element of bool M : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty I : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(I : ( ( ) ( ) set ) ,M : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) ) : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) ;
end;

definition
let I be ( ( ) ( ) set ) ;
let M be ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) ) ;
let IT be ( ( ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) MSSetOp of M : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) ) ) ;
attr IT is reflexive means :: CLOSURE1:def 1
 for X being ( ( ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) Element of bool M : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty I : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(I : ( ( ) ( ) set ) ,M : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) ) : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) holds X : ( ( ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) Element of bool M : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty I : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(I : ( ( ) ( ) set ) ,M : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) ) ) : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) c= IT : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) .. X : ( ( ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) Element of bool M : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty I : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(I : ( ( ) ( ) set ) ,M : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) ) ) : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) : ( ( ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) Element of bool M : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty I : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(I : ( ( ) ( ) set ) ,M : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) ) : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) ;
attr IT is monotonic means :: CLOSURE1:def 2
 for X, Y being ( ( ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) Element of bool M : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty I : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(I : ( ( ) ( ) set ) ,M : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) ) : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) st X : ( ( ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) Element of bool M : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty I : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(I : ( ( ) ( ) set ) ,M : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) ) ) : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) c= Y : ( ( ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) Element of bool M : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty I : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(I : ( ( ) ( ) set ) ,M : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) ) ) : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) holds
IT : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) .. X : ( ( ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) Element of bool M : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty I : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(I : ( ( ) ( ) set ) ,M : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) ) ) : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) : ( ( ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) Element of bool M : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty I : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(I : ( ( ) ( ) set ) ,M : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) ) : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) c= IT : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) .. Y : ( ( ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) Element of bool M : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty I : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(I : ( ( ) ( ) set ) ,M : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) ) ) : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) : ( ( ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) Element of bool M : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty I : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(I : ( ( ) ( ) set ) ,M : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) ) : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) ;
attr IT is idempotent means :: CLOSURE1:def 3
 for X being ( ( ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) Element of bool M : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty I : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(I : ( ( ) ( ) set ) ,M : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) ) : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) holds IT : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) .. X : ( ( ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) Element of bool M : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty I : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(I : ( ( ) ( ) set ) ,M : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) ) ) : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) : ( ( ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) Element of bool M : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty I : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(I : ( ( ) ( ) set ) ,M : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) ) : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) = IT : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) .. (IT : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) .. X : ( ( ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) Element of bool M : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty I : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(I : ( ( ) ( ) set ) ,M : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) ) ) : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) ) : ( ( ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) Element of bool M : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty I : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(I : ( ( ) ( ) set ) ,M : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) ) : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) : ( ( ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) Element of bool M : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty I : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(I : ( ( ) ( ) set ) ,M : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) ) : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) ;
attr IT is topological means :: CLOSURE1:def 4
 for X, Y being ( ( ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) Element of bool M : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty I : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(I : ( ( ) ( ) set ) ,M : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) ) : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) holds IT : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) .. (X : ( ( ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) Element of bool M : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty I : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(I : ( ( ) ( ) set ) ,M : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) ) ) : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) \/ Y : ( ( ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) Element of bool M : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty I : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(I : ( ( ) ( ) set ) ,M : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) ) ) : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) ) : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) = (IT : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) .. X : ( ( ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) Element of bool M : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty I : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(I : ( ( ) ( ) set ) ,M : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) ) ) : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) ) : ( ( ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) Element of bool M : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty I : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(I : ( ( ) ( ) set ) ,M : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) ) : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) \/ (IT : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) .. Y : ( ( ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) Element of bool M : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty I : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(I : ( ( ) ( ) set ) ,M : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) ) ) : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) ) : ( ( ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) Element of bool M : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty I : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(I : ( ( ) ( ) set ) ,M : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) ) : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) ;
end;

theorem :: CLOSURE1:8
for I being ( ( ) ( ) set )
for M being ( ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) )
for X being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) Element of M : ( ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) holds X : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) Element of b2 : ( ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) = (id M : ( ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) ManySortedFunction of b2 : ( ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b2 : ( ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) .. X : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) Element of b2 : ( ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) Element of b2 : ( ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) ;

theorem :: CLOSURE1:9
for I being ( ( ) ( ) set )
for M being ( ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) )
for X, Y being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) Element of M : ( ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) st X : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) Element of b2 : ( ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) c= Y : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) Element of b2 : ( ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) holds
(id M : ( ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) ManySortedFunction of b2 : ( ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b2 : ( ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) .. X : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) Element of b2 : ( ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) Element of b2 : ( ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) c= (id M : ( ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) ManySortedFunction of b2 : ( ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b2 : ( ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) .. Y : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) Element of b2 : ( ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) Element of b2 : ( ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) ;

theorem :: CLOSURE1:10
for I being ( ( ) ( ) set )
for M being ( ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) )
for X, Y being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) Element of M : ( ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) st X : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) Element of b2 : ( ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) \/ Y : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) Element of b2 : ( ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) is ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) Element of M : ( ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) holds
(id M : ( ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) ManySortedFunction of b2 : ( ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b2 : ( ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) .. (X : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) Element of b2 : ( ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) \/ Y : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) Element of b2 : ( ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) : ( ( Relation-like Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) = ((id M : ( ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) ManySortedFunction of b2 : ( ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b2 : ( ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) .. X : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) Element of b2 : ( ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) Element of b2 : ( ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) \/ ((id M : ( ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) ManySortedFunction of b2 : ( ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b2 : ( ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) .. Y : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) Element of b2 : ( ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) Element of b2 : ( ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ;

theorem :: CLOSURE1:11
for I being ( ( ) ( ) set )
for M being ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) )
for X being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) Element of bool M : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(b1 : ( ( ) ( ) set ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ) )
for i, x being ( ( ) ( ) set ) st i : ( ( ) ( ) set ) in I : ( ( ) ( ) set ) & x : ( ( ) ( ) set ) in ((id (bool M : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(b1 : ( ( ) ( ) set ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) ManySortedFunction of bool b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(b1 : ( ( ) ( ) set ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ) , bool b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(b1 : ( ( ) ( ) set ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) .. X : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) Element of bool b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(b1 : ( ( ) ( ) set ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) Element of bool b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(b1 : ( ( ) ( ) set ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) . i : ( ( ) ( ) set ) : ( ( ) ( ) set ) holds
ex Y being ( ( V42() ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total V42() ) Element of bool M : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(b1 : ( ( ) ( ) set ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) st
( Y : ( ( V42() ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total V42() ) Element of bool b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(b1 : ( ( ) ( ) set ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) c= X : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) Element of bool b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(b1 : ( ( ) ( ) set ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) & x : ( ( ) ( ) set ) in ((id (bool M : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(b1 : ( ( ) ( ) set ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) ManySortedFunction of bool b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(b1 : ( ( ) ( ) set ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ) , bool b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(b1 : ( ( ) ( ) set ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) .. Y : ( ( V42() ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total V42() ) Element of bool b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(b1 : ( ( ) ( ) set ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) Element of bool b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(b1 : ( ( ) ( ) set ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) . i : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ;

registration
let I be ( ( ) ( ) set ) ;
let M be ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) ) ;
cluster Relation-like I : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() reflexive monotonic idempotent topological for ( ( ) ( ) ManySortedFunction of bool M : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty I : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(I : ( ( ) ( ) set ) ,M : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) ) : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) ) , bool M : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty I : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(I : ( ( ) ( ) set ) ,M : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) ) : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) ;
end;

theorem :: CLOSURE1:12
for I being ( ( ) ( ) set )
for A being ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) ) holds id (bool A : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(b1 : ( ( ) ( ) set ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) ManySortedFunction of bool b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(b1 : ( ( ) ( ) set ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ) , bool b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(b1 : ( ( ) ( ) set ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) is ( ( reflexive ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() reflexive ) MSSetOp of A : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) ;

theorem :: CLOSURE1:13
for I being ( ( ) ( ) set )
for A being ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) ) holds id (bool A : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(b1 : ( ( ) ( ) set ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) ManySortedFunction of bool b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(b1 : ( ( ) ( ) set ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ) , bool b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(b1 : ( ( ) ( ) set ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) is ( ( monotonic ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() monotonic ) MSSetOp of A : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) ;

theorem :: CLOSURE1:14
for I being ( ( ) ( ) set )
for A being ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) ) holds id (bool A : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(b1 : ( ( ) ( ) set ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) ManySortedFunction of bool b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(b1 : ( ( ) ( ) set ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ) , bool b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(b1 : ( ( ) ( ) set ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) is ( ( idempotent ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() idempotent ) MSSetOp of A : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) ;

theorem :: CLOSURE1:15
for I being ( ( ) ( ) set )
for A being ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) ) holds id (bool A : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(b1 : ( ( ) ( ) set ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) ManySortedFunction of bool b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(b1 : ( ( ) ( ) set ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ) , bool b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(b1 : ( ( ) ( ) set ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) is ( ( topological ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() topological ) MSSetOp of A : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) ;

theorem :: CLOSURE1:16
for I being ( ( ) ( ) set )
for M being ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) )
for P being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) MSSetOp of M : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) )
for E being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) Element of bool M : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(b1 : ( ( ) ( ) set ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) st E : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) Element of bool b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(b1 : ( ( ) ( ) set ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) = M : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) & P : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) MSSetOp of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) is reflexive holds
E : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) Element of bool b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(b1 : ( ( ) ( ) set ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) = P : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) MSSetOp of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) .. E : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) Element of bool b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(b1 : ( ( ) ( ) set ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) Element of bool b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(b1 : ( ( ) ( ) set ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) ;

theorem :: CLOSURE1:17
for I being ( ( ) ( ) set )
for M being ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) )
for P being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) MSSetOp of M : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) st P : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) MSSetOp of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) is reflexive & ( for X being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) Element of bool M : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(b1 : ( ( ) ( ) set ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) holds P : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) MSSetOp of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) .. X : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) Element of bool b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(b1 : ( ( ) ( ) set ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) Element of bool b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(b1 : ( ( ) ( ) set ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) c= X : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) Element of bool b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(b1 : ( ( ) ( ) set ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) ) holds
P : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) MSSetOp of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) is idempotent ;

theorem :: CLOSURE1:18
for I being ( ( ) ( ) set )
for M being ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) )
for P being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) MSSetOp of M : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) )
for E, T being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) Element of bool M : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(b1 : ( ( ) ( ) set ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) st P : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) MSSetOp of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) is monotonic holds
P : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) MSSetOp of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) .. (E : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) Element of bool b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(b1 : ( ( ) ( ) set ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) /\ T : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) Element of bool b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(b1 : ( ( ) ( ) set ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) : ( ( Relation-like Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) c= (P : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) MSSetOp of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) .. E : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) Element of bool b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(b1 : ( ( ) ( ) set ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) Element of bool b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(b1 : ( ( ) ( ) set ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) /\ (P : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) MSSetOp of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) .. T : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) Element of bool b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(b1 : ( ( ) ( ) set ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) Element of bool b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(b1 : ( ( ) ( ) set ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ;

registration
let I be ( ( ) ( ) set ) ;
let M be ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) ) ;
cluster topological -> monotonic for ( ( ) ( ) ManySortedFunction of bool M : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty I : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(I : ( ( ) ( ) set ) ,M : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) ) : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) ) , bool M : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty I : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(I : ( ( ) ( ) set ) ,M : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) ) : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) ;
end;

theorem :: CLOSURE1:19
for I being ( ( ) ( ) set )
for M being ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) )
for P being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) MSSetOp of M : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) )
for E, T being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) Element of bool M : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(b1 : ( ( ) ( ) set ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) st P : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) MSSetOp of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) is topological holds
(P : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) MSSetOp of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) .. E : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) Element of bool b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(b1 : ( ( ) ( ) set ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) Element of bool b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(b1 : ( ( ) ( ) set ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) \ (P : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) MSSetOp of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) .. T : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) Element of bool b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(b1 : ( ( ) ( ) set ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) Element of bool b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(b1 : ( ( ) ( ) set ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) c= P : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) MSSetOp of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) .. (E : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) Element of bool b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(b1 : ( ( ) ( ) set ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) \ T : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) Element of bool b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(b1 : ( ( ) ( ) set ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) : ( ( Relation-like Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ;

definition
let I be ( ( ) ( ) set ) ;
let M be ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) ) ;
let R, P be ( ( ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) MSSetOp of M : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) ) ) ;
:: original: **
redefine func P ** R -> ( ( ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) MSSetOp of M : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ;
end;

theorem :: CLOSURE1:20
for I being ( ( ) ( ) set )
for M being ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) )
for P, R being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) MSSetOp of M : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) st P : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) MSSetOp of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) is reflexive & R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) MSSetOp of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) is reflexive holds
P : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) MSSetOp of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) ** R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) MSSetOp of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) MSSetOp of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) is reflexive ;

theorem :: CLOSURE1:21
for I being ( ( ) ( ) set )
for M being ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) )
for P, R being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) MSSetOp of M : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) st P : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) MSSetOp of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) is monotonic & R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) MSSetOp of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) is monotonic holds
P : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) MSSetOp of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) ** R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) MSSetOp of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) MSSetOp of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) is monotonic ;

theorem :: CLOSURE1:22
for I being ( ( ) ( ) set )
for M being ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) )
for P, R being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) MSSetOp of M : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) st P : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) MSSetOp of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) is idempotent & R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) MSSetOp of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) is idempotent & P : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) MSSetOp of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) ** R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) MSSetOp of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) MSSetOp of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) = R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) MSSetOp of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) ** P : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) MSSetOp of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) MSSetOp of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) holds
P : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) MSSetOp of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) ** R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) MSSetOp of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) MSSetOp of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) is idempotent ;

theorem :: CLOSURE1:23
for I being ( ( ) ( ) set )
for M being ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) )
for P, R being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) MSSetOp of M : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) st P : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) MSSetOp of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) is topological & R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) MSSetOp of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) is topological holds
P : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) MSSetOp of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) ** R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) MSSetOp of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) MSSetOp of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) is topological ;

theorem :: CLOSURE1:24
for i, I being ( ( ) ( ) set )
for M being ( ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) )
for f being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function)
for P being ( ( ) ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) MSSetOp of M : ( ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b2 : ( ( ) ( ) set ) ) ) st P : ( ( ) ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) MSSetOp of b3 : ( ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b2 : ( ( ) ( ) set ) ) ) is reflexive & i : ( ( ) ( ) set ) in I : ( ( ) ( ) set ) & f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) = P : ( ( ) ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) MSSetOp of b3 : ( ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b2 : ( ( ) ( ) set ) ) ) . i : ( ( ) ( ) set ) : ( ( ) ( Relation-like Function-like ) set ) holds
for x being ( ( ) ( ) Element of bool (M : ( ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b2 : ( ( ) ( ) set ) ) . i : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of K10(K10((b3 : ( ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b2 : ( ( ) ( ) set ) ) . b1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) holds x : ( ( ) ( ) Element of bool (b3 : ( ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b2 : ( ( ) ( ) set ) ) . b1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of K10(K10((b3 : ( ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b2 : ( ( ) ( ) set ) ) . b1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) c= f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) . x : ( ( ) ( ) Element of bool (b3 : ( ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b2 : ( ( ) ( ) set ) ) . b1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of K10(K10((b3 : ( ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b2 : ( ( ) ( ) set ) ) . b1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ;

theorem :: CLOSURE1:25
for i, I being ( ( ) ( ) set )
for M being ( ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) )
for f being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function)
for P being ( ( ) ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) MSSetOp of M : ( ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b2 : ( ( ) ( ) set ) ) ) st P : ( ( ) ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) MSSetOp of b3 : ( ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b2 : ( ( ) ( ) set ) ) ) is monotonic & i : ( ( ) ( ) set ) in I : ( ( ) ( ) set ) & f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) = P : ( ( ) ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) MSSetOp of b3 : ( ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b2 : ( ( ) ( ) set ) ) ) . i : ( ( ) ( ) set ) : ( ( ) ( Relation-like Function-like ) set ) holds
for x, y being ( ( ) ( ) Element of bool (M : ( ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b2 : ( ( ) ( ) set ) ) . i : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of K10(K10((b3 : ( ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b2 : ( ( ) ( ) set ) ) . b1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) st x : ( ( ) ( ) Element of bool (b3 : ( ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b2 : ( ( ) ( ) set ) ) . b1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of K10(K10((b3 : ( ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b2 : ( ( ) ( ) set ) ) . b1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) c= y : ( ( ) ( ) Element of bool (b3 : ( ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b2 : ( ( ) ( ) set ) ) . b1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of K10(K10((b3 : ( ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b2 : ( ( ) ( ) set ) ) . b1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) holds
f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) . x : ( ( ) ( ) Element of bool (b3 : ( ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b2 : ( ( ) ( ) set ) ) . b1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of K10(K10((b3 : ( ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b2 : ( ( ) ( ) set ) ) . b1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) c= f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) . y : ( ( ) ( ) Element of bool (b3 : ( ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b2 : ( ( ) ( ) set ) ) . b1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of K10(K10((b3 : ( ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b2 : ( ( ) ( ) set ) ) . b1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ;

theorem :: CLOSURE1:26
for i, I being ( ( ) ( ) set )
for M being ( ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) )
for f being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function)
for P being ( ( ) ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) MSSetOp of M : ( ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b2 : ( ( ) ( ) set ) ) ) st P : ( ( ) ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) MSSetOp of b3 : ( ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b2 : ( ( ) ( ) set ) ) ) is idempotent & i : ( ( ) ( ) set ) in I : ( ( ) ( ) set ) & f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) = P : ( ( ) ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) MSSetOp of b3 : ( ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b2 : ( ( ) ( ) set ) ) ) . i : ( ( ) ( ) set ) : ( ( ) ( Relation-like Function-like ) set ) holds
for x being ( ( ) ( ) Element of bool (M : ( ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b2 : ( ( ) ( ) set ) ) . i : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of K10(K10((b3 : ( ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b2 : ( ( ) ( ) set ) ) . b1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) holds f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) . x : ( ( ) ( ) Element of bool (b3 : ( ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b2 : ( ( ) ( ) set ) ) . b1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of K10(K10((b3 : ( ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b2 : ( ( ) ( ) set ) ) . b1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) = f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) . (f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) . x : ( ( ) ( ) Element of bool (b3 : ( ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b2 : ( ( ) ( ) set ) ) . b1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of K10(K10((b3 : ( ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b2 : ( ( ) ( ) set ) ) . b1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

theorem :: CLOSURE1:27
for i, I being ( ( ) ( ) set )
for M being ( ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) )
for f being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function)
for P being ( ( ) ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) MSSetOp of M : ( ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b2 : ( ( ) ( ) set ) ) ) st P : ( ( ) ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) MSSetOp of b3 : ( ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b2 : ( ( ) ( ) set ) ) ) is topological & i : ( ( ) ( ) set ) in I : ( ( ) ( ) set ) & f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) = P : ( ( ) ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) MSSetOp of b3 : ( ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b2 : ( ( ) ( ) set ) ) ) . i : ( ( ) ( ) set ) : ( ( ) ( Relation-like Function-like ) set ) holds
for x, y being ( ( ) ( ) Element of bool (M : ( ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b2 : ( ( ) ( ) set ) ) . i : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of K10(K10((b3 : ( ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b2 : ( ( ) ( ) set ) ) . b1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) holds f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) . (x : ( ( ) ( ) Element of bool (b3 : ( ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b2 : ( ( ) ( ) set ) ) . b1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of K10(K10((b3 : ( ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b2 : ( ( ) ( ) set ) ) . b1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) \/ y : ( ( ) ( ) Element of bool (b3 : ( ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b2 : ( ( ) ( ) set ) ) . b1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of K10(K10((b3 : ( ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b2 : ( ( ) ( ) set ) ) . b1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of K10((b3 : ( ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b2 : ( ( ) ( ) set ) ) . b1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) = (f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) . x : ( ( ) ( ) Element of bool (b3 : ( ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b2 : ( ( ) ( ) set ) ) . b1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of K10(K10((b3 : ( ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b2 : ( ( ) ( ) set ) ) . b1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) set ) \/ (f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) . y : ( ( ) ( ) Element of bool (b3 : ( ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b2 : ( ( ) ( ) set ) ) . b1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of K10(K10((b3 : ( ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b2 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b2 : ( ( ) ( ) set ) ) . b1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

begin

definition
let S be ( ( ) ( ) 1-sorted ) ;
attr c2 is strict ;
struct MSClosureStr over S -> ( ( ) ( ) many-sorted over S : ( ( ) ( ) 1-sorted ) ) ;
aggr MSClosureStr(# Sorts, Family #) -> ( ( strict ) ( strict ) MSClosureStr over S : ( ( ) ( ) 1-sorted ) ) ;
sel Family c2 -> ( ( ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) MSSubsetFamily of the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) ;
end;

definition
let S be ( ( ) ( ) 1-sorted ) ;
let IT be ( ( ) ( ) MSClosureStr over S : ( ( ) ( ) 1-sorted ) ) ;
attr IT is additive means :: CLOSURE1:def 5
 the Family of IT : ( ( Relation-like S : ( ( ) ( ) 1-sorted ) -defined Function-like total ) ( Relation-like S : ( ( ) ( ) 1-sorted ) -defined Function-like total ) set ) : ( ( ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) MSSubsetFamily of the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) is additive ;
attr IT is absolutely-additive means :: CLOSURE1:def 6
 the Family of IT : ( ( Relation-like S : ( ( ) ( ) 1-sorted ) -defined Function-like total ) ( Relation-like S : ( ( ) ( ) 1-sorted ) -defined Function-like total ) set ) : ( ( ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) MSSubsetFamily of the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) is absolutely-additive ;
attr IT is multiplicative means :: CLOSURE1:def 7
 the Family of IT : ( ( Relation-like S : ( ( ) ( ) 1-sorted ) -defined Function-like total ) ( Relation-like S : ( ( ) ( ) 1-sorted ) -defined Function-like total ) set ) : ( ( ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) MSSubsetFamily of the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) is multiplicative ;
attr IT is absolutely-multiplicative means :: CLOSURE1:def 8
 the Family of IT : ( ( Relation-like S : ( ( ) ( ) 1-sorted ) -defined Function-like total ) ( Relation-like S : ( ( ) ( ) 1-sorted ) -defined Function-like total ) set ) : ( ( ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) MSSubsetFamily of the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) is absolutely-multiplicative ;
attr IT is properly-upper-bound means :: CLOSURE1:def 9
 the Family of IT : ( ( Relation-like S : ( ( ) ( ) 1-sorted ) -defined Function-like total ) ( Relation-like S : ( ( ) ( ) 1-sorted ) -defined Function-like total ) set ) : ( ( ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) MSSubsetFamily of the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) is properly-upper-bound ;
attr IT is properly-lower-bound means :: CLOSURE1:def 10
 the Family of IT : ( ( Relation-like S : ( ( ) ( ) 1-sorted ) -defined Function-like total ) ( Relation-like S : ( ( ) ( ) 1-sorted ) -defined Function-like total ) set ) : ( ( ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) MSSubsetFamily of the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) is properly-lower-bound ;
end;

definition
let S be ( ( ) ( ) 1-sorted ) ;
let MS be ( ( ) ( ) many-sorted over S : ( ( ) ( ) 1-sorted ) ) ;
func MSFull MS -> ( ( ) ( ) MSClosureStr over S : ( ( ) ( ) 1-sorted ) ) equals :: CLOSURE1:def 11
 MSClosureStr(# the Sorts of MS : ( ( Relation-like S : ( ( ) ( ) 1-sorted ) -defined Function-like total ) ( Relation-like S : ( ( ) ( ) 1-sorted ) -defined Function-like total ) set ) : ( ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) set ) ,(bool the Sorts of MS : ( ( Relation-like S : ( ( ) ( ) 1-sorted ) -defined Function-like total ) ( Relation-like S : ( ( ) ( ) 1-sorted ) -defined Function-like total ) set ) : ( ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113( the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) , the Sorts of MS : ( ( Relation-like S : ( ( ) ( ) 1-sorted ) -defined Function-like total ) ( Relation-like S : ( ( ) ( ) 1-sorted ) -defined Function-like total ) set ) : ( ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) set ) ) : ( ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) set ) ) #) : ( ( strict ) ( strict ) MSClosureStr over S : ( ( ) ( ) 1-sorted ) ) ;
end;

registration
let S be ( ( ) ( ) 1-sorted ) ;
let MS be ( ( ) ( ) many-sorted over S : ( ( ) ( ) 1-sorted ) ) ;
cluster MSFull MS : ( ( ) ( ) many-sorted over S : ( ( ) ( ) 1-sorted ) ) : ( ( ) ( ) MSClosureStr over S : ( ( ) ( ) 1-sorted ) ) -> strict additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ;
end;

registration
let S be ( ( ) ( ) 1-sorted ) ;
let MS be ( ( non-empty ) ( non-empty ) many-sorted over S : ( ( ) ( ) 1-sorted ) ) ;
cluster MSFull MS : ( ( non-empty ) ( non-empty ) many-sorted over S : ( ( ) ( ) 1-sorted ) ) : ( ( ) ( strict additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) MSClosureStr over S : ( ( ) ( ) 1-sorted ) ) -> non-empty ;
end;

registration
let S be ( ( ) ( ) 1-sorted ) ;
cluster non-empty strict additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound for ( ( ) ( ) MSClosureStr over S : ( ( ) ( ) 1-sorted ) ) ;
end;

registration
let S be ( ( ) ( ) 1-sorted ) ;
let CS be ( ( additive ) ( additive ) MSClosureStr over S : ( ( ) ( ) 1-sorted ) ) ;
cluster the Family of CS : ( ( additive ) ( additive ) MSClosureStr over S : ( ( ) ( ) 1-sorted ) ) : ( ( ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) MSSubsetFamily of the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) -> additive ;
end;

registration
let S be ( ( ) ( ) 1-sorted ) ;
let CS be ( ( absolutely-additive ) ( absolutely-additive ) MSClosureStr over S : ( ( ) ( ) 1-sorted ) ) ;
cluster the Family of CS : ( ( absolutely-additive ) ( absolutely-additive ) MSClosureStr over S : ( ( ) ( ) 1-sorted ) ) : ( ( ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) MSSubsetFamily of the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) -> absolutely-additive ;
end;

registration
let S be ( ( ) ( ) 1-sorted ) ;
let CS be ( ( multiplicative ) ( multiplicative ) MSClosureStr over S : ( ( ) ( ) 1-sorted ) ) ;
cluster the Family of CS : ( ( multiplicative ) ( multiplicative ) MSClosureStr over S : ( ( ) ( ) 1-sorted ) ) : ( ( ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) MSSubsetFamily of the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) -> multiplicative ;
end;

registration
let S be ( ( ) ( ) 1-sorted ) ;
let CS be ( ( absolutely-multiplicative ) ( absolutely-multiplicative ) MSClosureStr over S : ( ( ) ( ) 1-sorted ) ) ;
cluster the Family of CS : ( ( absolutely-multiplicative ) ( absolutely-multiplicative ) MSClosureStr over S : ( ( ) ( ) 1-sorted ) ) : ( ( ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) MSSubsetFamily of the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) -> absolutely-multiplicative ;
end;

registration
let S be ( ( ) ( ) 1-sorted ) ;
let CS be ( ( properly-upper-bound ) ( properly-upper-bound ) MSClosureStr over S : ( ( ) ( ) 1-sorted ) ) ;
cluster the Family of CS : ( ( properly-upper-bound ) ( properly-upper-bound ) MSClosureStr over S : ( ( ) ( ) 1-sorted ) ) : ( ( ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) MSSubsetFamily of the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) -> properly-upper-bound ;
end;

registration
let S be ( ( ) ( ) 1-sorted ) ;
let CS be ( ( properly-lower-bound ) ( properly-lower-bound ) MSClosureStr over S : ( ( ) ( ) 1-sorted ) ) ;
cluster the Family of CS : ( ( properly-lower-bound ) ( properly-lower-bound ) MSClosureStr over S : ( ( ) ( ) 1-sorted ) ) : ( ( ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) MSSubsetFamily of the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) -> properly-lower-bound ;
end;

registration
let S be ( ( ) ( ) 1-sorted ) ;
let M be ( ( Relation-like V8() the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V8() the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) ;
let F be ( ( ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) MSSubsetFamily of the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) ;
cluster MSClosureStr(# M : ( ( Relation-like V8() the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V8() the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) set ) ,F : ( ( ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSubset of K113( the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ,M : ( ( Relation-like V8() the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V8() the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) set ) ) : ( ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) set ) ) #) : ( ( strict ) ( strict ) MSClosureStr over S : ( ( ) ( ) 1-sorted ) ) -> non-empty strict ;
end;

registration
let S be ( ( ) ( ) 1-sorted ) ;
let MS be ( ( ) ( ) many-sorted over S : ( ( ) ( ) 1-sorted ) ) ;
let F be ( ( additive ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total additive ) MSSubsetFamily of the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) ;
cluster MSClosureStr(# the Sorts of MS : ( ( ) ( ) many-sorted over S : ( ( ) ( ) 1-sorted ) ) : ( ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) set ) ,F : ( ( additive ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total additive ) ManySortedSubset of K113( the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) , the Sorts of MS : ( ( ) ( ) many-sorted over S : ( ( ) ( ) 1-sorted ) ) : ( ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) set ) ) : ( ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) set ) ) #) : ( ( strict ) ( strict ) MSClosureStr over S : ( ( ) ( ) 1-sorted ) ) -> strict additive ;
end;

registration
let S be ( ( ) ( ) 1-sorted ) ;
let MS be ( ( ) ( ) many-sorted over S : ( ( ) ( ) 1-sorted ) ) ;
let F be ( ( absolutely-additive ) ( Relation-like non-empty the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive properly-lower-bound ) MSSubsetFamily of the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) ;
cluster MSClosureStr(# the Sorts of MS : ( ( ) ( ) many-sorted over S : ( ( ) ( ) 1-sorted ) ) : ( ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) set ) ,F : ( ( absolutely-additive ) ( Relation-like non-empty the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive properly-lower-bound ) ManySortedSubset of K113( the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) , the Sorts of MS : ( ( ) ( ) many-sorted over S : ( ( ) ( ) 1-sorted ) ) : ( ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) set ) ) : ( ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) set ) ) #) : ( ( strict ) ( strict additive ) MSClosureStr over S : ( ( ) ( ) 1-sorted ) ) -> strict absolutely-additive ;
end;

registration
let S be ( ( ) ( ) 1-sorted ) ;
let MS be ( ( ) ( ) many-sorted over S : ( ( ) ( ) 1-sorted ) ) ;
let F be ( ( multiplicative ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total multiplicative ) MSSubsetFamily of the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) ;
cluster MSClosureStr(# the Sorts of MS : ( ( ) ( ) many-sorted over S : ( ( ) ( ) 1-sorted ) ) : ( ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) set ) ,F : ( ( multiplicative ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total multiplicative ) ManySortedSubset of K113( the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) , the Sorts of MS : ( ( ) ( ) many-sorted over S : ( ( ) ( ) 1-sorted ) ) : ( ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) set ) ) : ( ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) set ) ) #) : ( ( strict ) ( strict ) MSClosureStr over S : ( ( ) ( ) 1-sorted ) ) -> strict multiplicative ;
end;

registration
let S be ( ( ) ( ) 1-sorted ) ;
let MS be ( ( ) ( ) many-sorted over S : ( ( ) ( ) 1-sorted ) ) ;
let F be ( ( absolutely-multiplicative ) ( Relation-like non-empty the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total multiplicative absolutely-multiplicative properly-upper-bound ) MSSubsetFamily of the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) ;
cluster MSClosureStr(# the Sorts of MS : ( ( ) ( ) many-sorted over S : ( ( ) ( ) 1-sorted ) ) : ( ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) set ) ,F : ( ( absolutely-multiplicative ) ( Relation-like non-empty the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total multiplicative absolutely-multiplicative properly-upper-bound ) ManySortedSubset of K113( the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) , the Sorts of MS : ( ( ) ( ) many-sorted over S : ( ( ) ( ) 1-sorted ) ) : ( ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) set ) ) : ( ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) set ) ) #) : ( ( strict ) ( strict multiplicative ) MSClosureStr over S : ( ( ) ( ) 1-sorted ) ) -> strict absolutely-multiplicative ;
end;

registration
let S be ( ( ) ( ) 1-sorted ) ;
let MS be ( ( ) ( ) many-sorted over S : ( ( ) ( ) 1-sorted ) ) ;
let F be ( ( properly-upper-bound ) ( Relation-like non-empty the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total properly-upper-bound ) MSSubsetFamily of the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) ;
cluster MSClosureStr(# the Sorts of MS : ( ( ) ( ) many-sorted over S : ( ( ) ( ) 1-sorted ) ) : ( ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) set ) ,F : ( ( properly-upper-bound ) ( Relation-like non-empty the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total properly-upper-bound ) ManySortedSubset of K113( the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) , the Sorts of MS : ( ( ) ( ) many-sorted over S : ( ( ) ( ) 1-sorted ) ) : ( ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) set ) ) : ( ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) set ) ) #) : ( ( strict ) ( strict ) MSClosureStr over S : ( ( ) ( ) 1-sorted ) ) -> strict properly-upper-bound ;
end;

registration
let S be ( ( ) ( ) 1-sorted ) ;
let MS be ( ( ) ( ) many-sorted over S : ( ( ) ( ) 1-sorted ) ) ;
let F be ( ( properly-lower-bound ) ( Relation-like non-empty the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total properly-lower-bound ) MSSubsetFamily of the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) ;
cluster MSClosureStr(# the Sorts of MS : ( ( ) ( ) many-sorted over S : ( ( ) ( ) 1-sorted ) ) : ( ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) set ) ,F : ( ( properly-lower-bound ) ( Relation-like non-empty the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total properly-lower-bound ) ManySortedSubset of K113( the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) , the Sorts of MS : ( ( ) ( ) many-sorted over S : ( ( ) ( ) 1-sorted ) ) : ( ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) set ) ) : ( ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) set ) ) #) : ( ( strict ) ( strict ) MSClosureStr over S : ( ( ) ( ) 1-sorted ) ) -> strict properly-lower-bound ;
end;

registration
let S be ( ( ) ( ) 1-sorted ) ;
cluster absolutely-additive -> additive for ( ( ) ( ) MSClosureStr over S : ( ( ) ( ) 1-sorted ) ) ;
end;

registration
let S be ( ( ) ( ) 1-sorted ) ;
cluster absolutely-multiplicative -> multiplicative for ( ( ) ( ) MSClosureStr over S : ( ( ) ( ) 1-sorted ) ) ;
end;

registration
let S be ( ( ) ( ) 1-sorted ) ;
cluster absolutely-multiplicative -> properly-upper-bound for ( ( ) ( ) MSClosureStr over S : ( ( ) ( ) 1-sorted ) ) ;
end;

registration
let S be ( ( ) ( ) 1-sorted ) ;
cluster absolutely-additive -> properly-lower-bound for ( ( ) ( ) MSClosureStr over S : ( ( ) ( ) 1-sorted ) ) ;
end;

definition
let S be ( ( ) ( ) 1-sorted ) ;
mode MSClosureSystem of S is ( ( absolutely-multiplicative ) ( multiplicative absolutely-multiplicative properly-upper-bound ) MSClosureStr over S : ( ( ) ( ) 1-sorted ) ) ;
end;

definition
let I be ( ( ) ( ) set ) ;
let M be ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) ) ;
mode MSClosureOperator of M is ( ( reflexive monotonic idempotent ) ( Relation-like I : ( ( ) ( ) 1-sorted ) -defined Function-like total Function-yielding V25() reflexive monotonic idempotent ) MSSetOp of M : ( ( Relation-like I : ( ( ) ( ) 1-sorted ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) 1-sorted ) -defined Function-like total ) set ) ) ;
end;

definition
let I be ( ( ) ( ) set ) ;
let M be ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) ) ;
let F be ( ( ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) ManySortedFunction of M : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) ) ,M : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) ) ) ;
func MSFixPoints F -> ( ( ) ( Relation-like I : ( ( ) ( ) 1-sorted ) -defined Function-like total ) ManySortedSubset of M : ( ( Relation-like I : ( ( ) ( ) 1-sorted ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) 1-sorted ) -defined Function-like total ) set ) ) means :: CLOSURE1:def 12
 for x, i being ( ( ) ( ) set ) st i : ( ( ) ( ) set ) in I : ( ( ) ( ) 1-sorted ) holds
( x : ( ( ) ( ) set ) in it : ( ( Function-like V21(M : ( ( Relation-like I : ( ( ) ( ) 1-sorted ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) 1-sorted ) -defined Function-like total ) set ) ,I : ( ( ) ( ) 1-sorted ) ) ) ( Relation-like M : ( ( Relation-like I : ( ( ) ( ) 1-sorted ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) 1-sorted ) -defined Function-like total ) set ) -defined I : ( ( ) ( ) 1-sorted ) -valued Function-like V21(M : ( ( Relation-like I : ( ( ) ( ) 1-sorted ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) 1-sorted ) -defined Function-like total ) set ) ,I : ( ( ) ( ) 1-sorted ) ) ) Element of K10(K11(M : ( ( Relation-like I : ( ( ) ( ) 1-sorted ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) 1-sorted ) -defined Function-like total ) set ) ,I : ( ( ) ( ) 1-sorted ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( non empty ) set ) ) . i : ( ( ) ( ) set ) : ( ( ) ( ) set ) iff ex f being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) st
( f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) = F : ( ( properly-lower-bound ) ( Relation-like non-empty the carrier of I : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total properly-lower-bound ) ManySortedSubset of K113( the carrier of I : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) , the Sorts of M : ( ( Relation-like I : ( ( ) ( ) 1-sorted ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) 1-sorted ) -defined Function-like total ) set ) : ( ( Relation-like the carrier of I : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of I : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) set ) ) : ( ( Relation-like the carrier of I : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of I : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) set ) ) . i : ( ( ) ( ) set ) : ( ( ) ( ) set ) & x : ( ( ) ( ) set ) in dom f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) & f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) . x : ( ( ) ( ) set ) : ( ( ) ( ) set ) = x : ( ( ) ( ) set ) ) );
end;

registration
let I be ( ( ) ( ) set ) ;
let M be ( ( Relation-like V9() I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V9() I : ( ( ) ( ) set ) -defined Function-like total finite-yielding ) ManySortedSet of I : ( ( ) ( ) set ) ) ;
let F be ( ( ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) ManySortedFunction of M : ( ( Relation-like V9() I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V9() I : ( ( ) ( ) set ) -defined Function-like total finite-yielding ) ManySortedSet of I : ( ( ) ( ) set ) ) ,M : ( ( Relation-like V9() I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V9() I : ( ( ) ( ) set ) -defined Function-like total finite-yielding ) ManySortedSet of I : ( ( ) ( ) set ) ) ) ;
cluster MSFixPoints F : ( ( ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) ManySortedFunction of M : ( ( Relation-like V9() I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V9() I : ( ( ) ( ) set ) -defined Function-like total finite-yielding ) set ) ,M : ( ( Relation-like V9() I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V9() I : ( ( ) ( ) set ) -defined Function-like total finite-yielding ) set ) ) : ( ( ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total finite-yielding ) ManySortedSubset of M : ( ( Relation-like V9() I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V9() I : ( ( ) ( ) set ) -defined Function-like total finite-yielding ) set ) ) -> V9() ;
end;

theorem :: CLOSURE1:28
for I being ( ( ) ( ) set )
for M, A being ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) )
for F being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) ManySortedFunction of M : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,M : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) holds
( ( A : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) in M : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) & F : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) ManySortedFunction of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) .. A : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) = A : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) iff A : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) in MSFixPoints F : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) ManySortedFunction of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSubset of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) ) ;

theorem :: CLOSURE1:29
for I being ( ( ) ( ) set )
for A being ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) ) holds MSFixPoints (id A : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) ManySortedFunction of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSubset of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) = A : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ;

theorem :: CLOSURE1:30
for S being ( ( ) ( ) 1-sorted )
for A being ( ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) )
for J being ( ( reflexive monotonic ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() reflexive monotonic ) MSSetOp of A : ( ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) )
for D being ( ( ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) MSSubsetFamily of the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) st D : ( ( ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) MSSubsetFamily of the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) = MSFixPoints J : ( ( reflexive monotonic ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() reflexive monotonic ) MSSetOp of b2 : ( ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSubset of bool b2 : ( ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113( the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ,b2 : ( ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) ) : ( ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) holds
MSClosureStr(# A : ( ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) ,D : ( ( ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) MSSubsetFamily of the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) #) : ( ( strict ) ( strict ) MSClosureStr over b1 : ( ( ) ( ) 1-sorted ) ) is ( ( absolutely-multiplicative ) ( multiplicative absolutely-multiplicative properly-upper-bound ) MSClosureSystem of S : ( ( ) ( ) 1-sorted ) ) ;

theorem :: CLOSURE1:31
for I being ( ( ) ( ) set )
for M being ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) )
for D being ( ( properly-upper-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total properly-upper-bound ) MSSubsetFamily of I : ( ( ) ( ) set ) )
for X being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) Element of bool M : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(b1 : ( ( ) ( ) set ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) ex SF being ( ( V8() ) ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) MSSubsetFamily of I : ( ( ) ( ) set ) ) st
for Y being ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) ) holds
( Y : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) in SF : ( ( V8() ) ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) MSSubsetFamily of b1 : ( ( ) ( ) set ) ) iff ( Y : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) in D : ( ( properly-upper-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total properly-upper-bound ) MSSubsetFamily of b1 : ( ( ) ( ) set ) ) & X : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) Element of bool b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(b1 : ( ( ) ( ) set ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) c= Y : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) ) ;

theorem :: CLOSURE1:32
for I being ( ( ) ( ) set )
for M being ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) )
for D being ( ( properly-upper-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total properly-upper-bound ) MSSubsetFamily of I : ( ( ) ( ) set ) )
for X being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) Element of bool M : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(b1 : ( ( ) ( ) set ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ) )
for SF being ( ( V8() ) ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) MSSubsetFamily of I : ( ( ) ( ) set ) ) st ( for Y being ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) ) holds
( Y : ( ( ) ( ) set ) in SF : ( ( V8() ) ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) MSSubsetFamily of b1 : ( ( ) ( ) set ) ) iff ( Y : ( ( ) ( ) set ) in D : ( ( properly-upper-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total properly-upper-bound ) MSSubsetFamily of b1 : ( ( ) ( ) set ) ) & X : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) Element of bool b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(b1 : ( ( ) ( ) set ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) c= Y : ( ( ) ( ) set ) ) ) ) holds
for i being ( ( ) ( ) set )
for Di being ( ( non empty ) ( non empty ) set ) st i : ( ( ) ( ) set ) in I : ( ( ) ( ) set ) & Di : ( ( non empty ) ( non empty ) set ) = D : ( ( properly-upper-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total properly-upper-bound ) MSSubsetFamily of b1 : ( ( ) ( ) set ) ) . i : ( ( ) ( ) set ) : ( ( ) ( ) set ) holds
SF : ( ( V8() ) ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) MSSubsetFamily of b1 : ( ( ) ( ) set ) ) . i : ( ( ) ( ) set ) : ( ( ) ( ) set ) = { z : ( ( ) ( ) Element of b7 : ( ( non empty ) ( non empty ) set ) ) where z is ( ( ) ( ) Element of Di : ( ( non empty ) ( non empty ) set ) ) : X : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) Element of bool b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(b1 : ( ( ) ( ) set ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) . i : ( ( ) ( ) set ) : ( ( ) ( ) set ) c= z : ( ( ) ( ) Element of b7 : ( ( non empty ) ( non empty ) set ) ) } ;

theorem :: CLOSURE1:33
for I being ( ( ) ( ) set )
for M being ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) )
for D being ( ( properly-upper-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total properly-upper-bound ) MSSubsetFamily of I : ( ( ) ( ) set ) ) ex J being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) MSSetOp of M : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) st
for X being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) Element of bool M : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(b1 : ( ( ) ( ) set ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ) )
for SF being ( ( V8() ) ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) MSSubsetFamily of I : ( ( ) ( ) set ) ) st ( for Y being ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) ) holds
( Y : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) in SF : ( ( V8() ) ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) MSSubsetFamily of b1 : ( ( ) ( ) set ) ) iff ( Y : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) in D : ( ( properly-upper-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total properly-upper-bound ) MSSubsetFamily of b1 : ( ( ) ( ) set ) ) & X : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) Element of bool b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(b1 : ( ( ) ( ) set ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) c= Y : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) ) ) holds
J : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) MSSetOp of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) .. X : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) Element of bool b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(b1 : ( ( ) ( ) set ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) Element of bool b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(b1 : ( ( ) ( ) set ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) = meet SF : ( ( V8() ) ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) MSSubsetFamily of b1 : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSubset of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) ;

theorem :: CLOSURE1:34
for I being ( ( ) ( ) set )
for M being ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) )
for D being ( ( properly-upper-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total properly-upper-bound ) MSSubsetFamily of I : ( ( ) ( ) set ) )
for A being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) Element of bool M : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(b1 : ( ( ) ( ) set ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ) )
for J being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) MSSetOp of M : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) st A : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) Element of bool b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(b1 : ( ( ) ( ) set ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) in D : ( ( properly-upper-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total properly-upper-bound ) MSSubsetFamily of b1 : ( ( ) ( ) set ) ) & ( for X being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) Element of bool M : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(b1 : ( ( ) ( ) set ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ) )
for SF being ( ( V8() ) ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) MSSubsetFamily of I : ( ( ) ( ) set ) ) st ( for Y being ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) ) holds
( Y : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) in SF : ( ( V8() ) ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) MSSubsetFamily of b1 : ( ( ) ( ) set ) ) iff ( Y : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) in D : ( ( properly-upper-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total properly-upper-bound ) MSSubsetFamily of b1 : ( ( ) ( ) set ) ) & X : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) Element of bool b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(b1 : ( ( ) ( ) set ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) c= Y : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) ) ) holds
J : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) MSSetOp of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) .. X : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) Element of bool b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(b1 : ( ( ) ( ) set ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) Element of bool b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(b1 : ( ( ) ( ) set ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) = meet SF : ( ( V8() ) ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) MSSubsetFamily of b1 : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSubset of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) ) holds
J : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) MSSetOp of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) .. A : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) Element of bool b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(b1 : ( ( ) ( ) set ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) Element of bool b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(b1 : ( ( ) ( ) set ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) = A : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) Element of bool b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(b1 : ( ( ) ( ) set ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) ;

theorem :: CLOSURE1:35
for I being ( ( ) ( ) set )
for M being ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) )
for D being ( ( absolutely-multiplicative ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total multiplicative absolutely-multiplicative properly-upper-bound ) MSSubsetFamily of I : ( ( ) ( ) set ) )
for A being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) Element of bool M : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(b1 : ( ( ) ( ) set ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ) )
for J being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) MSSetOp of M : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) st J : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) MSSetOp of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) .. A : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) Element of bool b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(b1 : ( ( ) ( ) set ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) Element of bool b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(b1 : ( ( ) ( ) set ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) = A : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) Element of bool b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(b1 : ( ( ) ( ) set ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) & ( for X being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) Element of bool M : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(b1 : ( ( ) ( ) set ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ) )
for SF being ( ( V8() ) ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) MSSubsetFamily of I : ( ( ) ( ) set ) ) st ( for Y being ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) ) holds
( Y : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) in SF : ( ( V8() ) ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) MSSubsetFamily of b1 : ( ( ) ( ) set ) ) iff ( Y : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) in D : ( ( absolutely-multiplicative ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total multiplicative absolutely-multiplicative properly-upper-bound ) MSSubsetFamily of b1 : ( ( ) ( ) set ) ) & X : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) Element of bool b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(b1 : ( ( ) ( ) set ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) c= Y : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) ) ) holds
J : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) MSSetOp of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) .. X : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) Element of bool b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(b1 : ( ( ) ( ) set ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) Element of bool b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(b1 : ( ( ) ( ) set ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) = meet SF : ( ( V8() ) ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) MSSubsetFamily of b1 : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSubset of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) ) holds
A : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) Element of bool b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(b1 : ( ( ) ( ) set ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) in D : ( ( absolutely-multiplicative ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total multiplicative absolutely-multiplicative properly-upper-bound ) MSSubsetFamily of b1 : ( ( ) ( ) set ) ) ;

theorem :: CLOSURE1:36
for I being ( ( ) ( ) set )
for M being ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) )
for D being ( ( properly-upper-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total properly-upper-bound ) MSSubsetFamily of I : ( ( ) ( ) set ) )
for J being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) MSSetOp of M : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) st ( for X being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) Element of bool M : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(b1 : ( ( ) ( ) set ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ) )
for SF being ( ( V8() ) ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) MSSubsetFamily of I : ( ( ) ( ) set ) ) st ( for Y being ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) ) holds
( Y : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) in SF : ( ( V8() ) ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) MSSubsetFamily of b1 : ( ( ) ( ) set ) ) iff ( Y : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) in D : ( ( properly-upper-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total properly-upper-bound ) MSSubsetFamily of b1 : ( ( ) ( ) set ) ) & X : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) Element of bool b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(b1 : ( ( ) ( ) set ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) c= Y : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) ) ) holds
J : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) MSSetOp of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) .. X : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) Element of bool b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(b1 : ( ( ) ( ) set ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) Element of bool b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(b1 : ( ( ) ( ) set ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) = meet SF : ( ( V8() ) ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) MSSubsetFamily of b1 : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSubset of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) ) holds
( J : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) MSSetOp of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) is reflexive & J : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) MSSetOp of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) is monotonic ) ;

theorem :: CLOSURE1:37
for I being ( ( ) ( ) set )
for M being ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) )
for D being ( ( absolutely-multiplicative ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total multiplicative absolutely-multiplicative properly-upper-bound ) MSSubsetFamily of I : ( ( ) ( ) set ) )
for J being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) MSSetOp of M : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) st ( for X being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) Element of bool M : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(b1 : ( ( ) ( ) set ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ) )
for SF being ( ( V8() ) ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) MSSubsetFamily of I : ( ( ) ( ) set ) ) st ( for Y being ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of I : ( ( ) ( ) set ) ) holds
( Y : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) in SF : ( ( V8() ) ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) MSSubsetFamily of b1 : ( ( ) ( ) set ) ) iff ( Y : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) in D : ( ( absolutely-multiplicative ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total multiplicative absolutely-multiplicative properly-upper-bound ) MSSubsetFamily of b1 : ( ( ) ( ) set ) ) & X : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) Element of bool b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(b1 : ( ( ) ( ) set ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) c= Y : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) ) ) holds
J : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) MSSetOp of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) .. X : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) Element of bool b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(b1 : ( ( ) ( ) set ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) Element of bool b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty b1 : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113(b1 : ( ( ) ( ) set ) ,b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) = meet SF : ( ( V8() ) ( Relation-like V8() b1 : ( ( ) ( ) set ) -defined Function-like total ) MSSubsetFamily of b1 : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSubset of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) ) holds
J : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) MSSetOp of b2 : ( ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of b1 : ( ( ) ( ) set ) ) ) is idempotent ;

theorem :: CLOSURE1:38
for S being ( ( ) ( ) 1-sorted )
for D being ( ( absolutely-multiplicative ) ( multiplicative absolutely-multiplicative properly-upper-bound ) MSClosureSystem of S : ( ( ) ( ) 1-sorted ) )
for J being ( ( ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) MSSetOp of the Sorts of D : ( ( absolutely-multiplicative ) ( multiplicative absolutely-multiplicative properly-upper-bound ) MSClosureSystem of b1 : ( ( ) ( ) 1-sorted ) ) : ( ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) set ) ) st ( for X being ( ( ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) Element of bool the Sorts of D : ( ( absolutely-multiplicative ) ( multiplicative absolutely-multiplicative properly-upper-bound ) MSClosureSystem of b1 : ( ( ) ( ) 1-sorted ) ) : ( ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) set ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113( the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) , the Sorts of b2 : ( ( absolutely-multiplicative ) ( multiplicative absolutely-multiplicative properly-upper-bound ) MSClosureSystem of b1 : ( ( ) ( ) 1-sorted ) ) : ( ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) set ) ) : ( ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) set ) ) )
for SF being ( ( V8() ) ( Relation-like V8() the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) MSSubsetFamily of the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) st ( for Y being ( ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) holds
( Y : ( ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) in SF : ( ( V8() ) ( Relation-like V8() the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) MSSubsetFamily of the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) iff ( Y : ( ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) in the Family of D : ( ( absolutely-multiplicative ) ( multiplicative absolutely-multiplicative properly-upper-bound ) MSClosureSystem of b1 : ( ( ) ( ) 1-sorted ) ) : ( ( ) ( Relation-like non-empty the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total multiplicative absolutely-multiplicative properly-upper-bound ) MSSubsetFamily of the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) & X : ( ( ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) Element of bool the Sorts of b2 : ( ( absolutely-multiplicative ) ( multiplicative absolutely-multiplicative properly-upper-bound ) MSClosureSystem of b1 : ( ( ) ( ) 1-sorted ) ) : ( ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) set ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113( the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) , the Sorts of b2 : ( ( absolutely-multiplicative ) ( multiplicative absolutely-multiplicative properly-upper-bound ) MSClosureSystem of b1 : ( ( ) ( ) 1-sorted ) ) : ( ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) set ) ) : ( ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) c= Y : ( ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) ) ) ) holds
J : ( ( ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) MSSetOp of the Sorts of b2 : ( ( absolutely-multiplicative ) ( multiplicative absolutely-multiplicative properly-upper-bound ) MSClosureSystem of b1 : ( ( ) ( ) 1-sorted ) ) : ( ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) set ) ) .. X : ( ( ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) Element of bool the Sorts of b2 : ( ( absolutely-multiplicative ) ( multiplicative absolutely-multiplicative properly-upper-bound ) MSClosureSystem of b1 : ( ( ) ( ) 1-sorted ) ) : ( ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) set ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113( the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) , the Sorts of b2 : ( ( absolutely-multiplicative ) ( multiplicative absolutely-multiplicative properly-upper-bound ) MSClosureSystem of b1 : ( ( ) ( ) 1-sorted ) ) : ( ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) set ) ) : ( ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) : ( ( ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) Element of bool the Sorts of b2 : ( ( absolutely-multiplicative ) ( multiplicative absolutely-multiplicative properly-upper-bound ) MSClosureSystem of b1 : ( ( ) ( ) 1-sorted ) ) : ( ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) set ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113( the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) , the Sorts of b2 : ( ( absolutely-multiplicative ) ( multiplicative absolutely-multiplicative properly-upper-bound ) MSClosureSystem of b1 : ( ( ) ( ) 1-sorted ) ) : ( ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) set ) ) : ( ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) = meet SF : ( ( V8() ) ( Relation-like V8() the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) MSSubsetFamily of the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSubset of the Sorts of b2 : ( ( absolutely-multiplicative ) ( multiplicative absolutely-multiplicative properly-upper-bound ) MSClosureSystem of b1 : ( ( ) ( ) 1-sorted ) ) : ( ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) holds
J : ( ( ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() ) MSSetOp of the Sorts of b2 : ( ( absolutely-multiplicative ) ( multiplicative absolutely-multiplicative properly-upper-bound ) MSClosureSystem of b1 : ( ( ) ( ) 1-sorted ) ) : ( ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) set ) ) is ( ( reflexive monotonic idempotent ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() reflexive monotonic idempotent ) MSClosureOperator of the Sorts of D : ( ( absolutely-multiplicative ) ( multiplicative absolutely-multiplicative properly-upper-bound ) MSClosureSystem of b1 : ( ( ) ( ) 1-sorted ) ) : ( ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ;

definition
let S be ( ( ) ( ) 1-sorted ) ;
let A be ( ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) ;
let C be ( ( reflexive monotonic idempotent ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() reflexive monotonic idempotent ) MSClosureOperator of A : ( ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) ) ;
func ClOp->ClSys C -> ( ( absolutely-multiplicative ) ( multiplicative absolutely-multiplicative properly-upper-bound ) MSClosureSystem of S : ( ( ) ( ) 1-sorted ) ) means :: CLOSURE1:def 13
 ex D being ( ( ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) MSSubsetFamily of the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) st
( D : ( ( ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) MSSubsetFamily of the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) = MSFixPoints C : ( ( ) ( Relation-like S : ( ( ) ( ) 1-sorted ) -defined Function-like total Function-yielding V25() ) ManySortedFunction of A : ( ( Relation-like S : ( ( ) ( ) 1-sorted ) -defined Function-like total ) ( Relation-like S : ( ( ) ( ) 1-sorted ) -defined Function-like total ) set ) ,A : ( ( Relation-like S : ( ( ) ( ) 1-sorted ) -defined Function-like total ) ( Relation-like S : ( ( ) ( ) 1-sorted ) -defined Function-like total ) set ) ) : ( ( ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSubset of bool A : ( ( Relation-like S : ( ( ) ( ) 1-sorted ) -defined Function-like total ) ( Relation-like S : ( ( ) ( ) 1-sorted ) -defined Function-like total ) set ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113( the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ,A : ( ( Relation-like S : ( ( ) ( ) 1-sorted ) -defined Function-like total ) ( Relation-like S : ( ( ) ( ) 1-sorted ) -defined Function-like total ) set ) ) : ( ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) & it : ( ( Function-like V21(A : ( ( Relation-like S : ( ( ) ( ) 1-sorted ) -defined Function-like total ) ( Relation-like S : ( ( ) ( ) 1-sorted ) -defined Function-like total ) set ) ,S : ( ( ) ( ) 1-sorted ) ) ) ( Relation-like A : ( ( Relation-like S : ( ( ) ( ) 1-sorted ) -defined Function-like total ) ( Relation-like S : ( ( ) ( ) 1-sorted ) -defined Function-like total ) set ) -defined S : ( ( ) ( ) 1-sorted ) -valued Function-like V21(A : ( ( Relation-like S : ( ( ) ( ) 1-sorted ) -defined Function-like total ) ( Relation-like S : ( ( ) ( ) 1-sorted ) -defined Function-like total ) set ) ,S : ( ( ) ( ) 1-sorted ) ) ) Element of K10(K11(A : ( ( Relation-like S : ( ( ) ( ) 1-sorted ) -defined Function-like total ) ( Relation-like S : ( ( ) ( ) 1-sorted ) -defined Function-like total ) set ) ,S : ( ( ) ( ) 1-sorted ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( non empty ) set ) ) = MSClosureStr(# A : ( ( Relation-like S : ( ( ) ( ) 1-sorted ) -defined Function-like total ) ( Relation-like S : ( ( ) ( ) 1-sorted ) -defined Function-like total ) set ) ,D : ( ( ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) MSSubsetFamily of the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) #) : ( ( strict ) ( strict ) MSClosureStr over S : ( ( ) ( ) 1-sorted ) ) );
end;

registration
let S be ( ( ) ( ) 1-sorted ) ;
let A be ( ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) ;
let C be ( ( reflexive monotonic idempotent ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() reflexive monotonic idempotent ) MSClosureOperator of A : ( ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) ) ;
cluster ClOp->ClSys C : ( ( reflexive monotonic idempotent ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() reflexive monotonic idempotent ) ManySortedFunction of bool A : ( ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) set ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113( the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ,A : ( ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) set ) ) : ( ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) set ) ) , bool A : ( ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) set ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113( the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ,A : ( ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) set ) ) : ( ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) : ( ( absolutely-multiplicative ) ( multiplicative absolutely-multiplicative properly-upper-bound ) MSClosureSystem of S : ( ( ) ( ) 1-sorted ) ) -> strict absolutely-multiplicative ;
end;

registration
let S be ( ( ) ( ) 1-sorted ) ;
let A be ( ( Relation-like V8() the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V8() the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) ;
let C be ( ( reflexive monotonic idempotent ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() reflexive monotonic idempotent ) MSClosureOperator of A : ( ( Relation-like V8() the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V8() the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) ) ;
cluster ClOp->ClSys C : ( ( reflexive monotonic idempotent ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() reflexive monotonic idempotent ) ManySortedFunction of bool A : ( ( Relation-like V8() the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V8() the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) set ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113( the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ,A : ( ( Relation-like V8() the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V8() the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) set ) ) : ( ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) set ) ) , bool A : ( ( Relation-like V8() the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V8() the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) set ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113( the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ,A : ( ( Relation-like V8() the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like V8() the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) set ) ) : ( ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) : ( ( absolutely-multiplicative ) ( strict multiplicative absolutely-multiplicative properly-upper-bound ) MSClosureSystem of S : ( ( ) ( ) 1-sorted ) ) -> non-empty absolutely-multiplicative ;
end;

definition
let S be ( ( ) ( ) 1-sorted ) ;
let D be ( ( absolutely-multiplicative ) ( multiplicative absolutely-multiplicative properly-upper-bound ) MSClosureSystem of S : ( ( ) ( ) 1-sorted ) ) ;
func ClSys->ClOp D -> ( ( reflexive monotonic idempotent ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() reflexive monotonic idempotent ) MSClosureOperator of the Sorts of D : ( ( Relation-like S : ( ( ) ( ) 1-sorted ) -defined Function-like total ) ( Relation-like S : ( ( ) ( ) 1-sorted ) -defined Function-like total ) set ) : ( ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) set ) ) means :: CLOSURE1:def 14
 for X being ( ( ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) Element of bool the Sorts of D : ( ( Relation-like S : ( ( ) ( ) 1-sorted ) -defined Function-like total ) ( Relation-like S : ( ( ) ( ) 1-sorted ) -defined Function-like total ) set ) : ( ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) set ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113( the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) , the Sorts of D : ( ( Relation-like S : ( ( ) ( ) 1-sorted ) -defined Function-like total ) ( Relation-like S : ( ( ) ( ) 1-sorted ) -defined Function-like total ) set ) : ( ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) set ) ) : ( ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) set ) ) )
for SF being ( ( V8() ) ( Relation-like V8() the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) MSSubsetFamily of the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) st ( for Y being ( ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) holds
( Y : ( ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) in SF : ( ( V8() ) ( Relation-like V8() the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) MSSubsetFamily of the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) iff ( Y : ( ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) in the Family of D : ( ( Relation-like S : ( ( ) ( ) 1-sorted ) -defined Function-like total ) ( Relation-like S : ( ( ) ( ) 1-sorted ) -defined Function-like total ) set ) : ( ( ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) MSSubsetFamily of the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) & X : ( ( ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) Element of bool the Sorts of D : ( ( absolutely-multiplicative ) ( multiplicative absolutely-multiplicative properly-upper-bound ) MSClosureSystem of S : ( ( ) ( ) 1-sorted ) ) : ( ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) set ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113( the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) , the Sorts of D : ( ( absolutely-multiplicative ) ( multiplicative absolutely-multiplicative properly-upper-bound ) MSClosureSystem of S : ( ( ) ( ) 1-sorted ) ) : ( ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) set ) ) : ( ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) c= Y : ( ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) ) ) ) holds
it : ( ( reflexive monotonic idempotent ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() reflexive monotonic idempotent ) ManySortedFunction of bool D : ( ( Relation-like S : ( ( ) ( ) 1-sorted ) -defined Function-like total ) ( Relation-like S : ( ( ) ( ) 1-sorted ) -defined Function-like total ) set ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113( the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ,D : ( ( Relation-like S : ( ( ) ( ) 1-sorted ) -defined Function-like total ) ( Relation-like S : ( ( ) ( ) 1-sorted ) -defined Function-like total ) set ) ) : ( ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) set ) ) , bool D : ( ( Relation-like S : ( ( ) ( ) 1-sorted ) -defined Function-like total ) ( Relation-like S : ( ( ) ( ) 1-sorted ) -defined Function-like total ) set ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113( the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ,D : ( ( Relation-like S : ( ( ) ( ) 1-sorted ) -defined Function-like total ) ( Relation-like S : ( ( ) ( ) 1-sorted ) -defined Function-like total ) set ) ) : ( ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) .. X : ( ( ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) Element of bool the Sorts of D : ( ( absolutely-multiplicative ) ( multiplicative absolutely-multiplicative properly-upper-bound ) MSClosureSystem of S : ( ( ) ( ) 1-sorted ) ) : ( ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) set ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113( the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) , the Sorts of D : ( ( absolutely-multiplicative ) ( multiplicative absolutely-multiplicative properly-upper-bound ) MSClosureSystem of S : ( ( ) ( ) 1-sorted ) ) : ( ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) set ) ) : ( ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) : ( ( ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) Element of bool the Sorts of D : ( ( Relation-like S : ( ( ) ( ) 1-sorted ) -defined Function-like total ) ( Relation-like S : ( ( ) ( ) 1-sorted ) -defined Function-like total ) set ) : ( ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) set ) : ( ( additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ( Relation-like non-empty the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ) ManySortedSubset of K113( the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) , the Sorts of D : ( ( Relation-like S : ( ( ) ( ) 1-sorted ) -defined Function-like total ) ( Relation-like S : ( ( ) ( ) 1-sorted ) -defined Function-like total ) set ) : ( ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) set ) ) : ( ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ) = meet SF : ( ( V8() ) ( Relation-like V8() the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) MSSubsetFamily of the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSubset of the Sorts of D : ( ( Relation-like S : ( ( ) ( ) 1-sorted ) -defined Function-like total ) ( Relation-like S : ( ( ) ( ) 1-sorted ) -defined Function-like total ) set ) : ( ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) set ) ) ;
end;

theorem :: CLOSURE1:39
for S being ( ( ) ( ) 1-sorted )
for A being ( ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) )
for J being ( ( reflexive monotonic idempotent ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() reflexive monotonic idempotent ) MSClosureOperator of A : ( ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) ) holds ClSys->ClOp (ClOp->ClSys J : ( ( reflexive monotonic idempotent ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() reflexive monotonic idempotent ) MSClosureOperator of b2 : ( ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) ) ) : ( ( absolutely-multiplicative ) ( strict multiplicative absolutely-multiplicative properly-upper-bound ) MSClosureSystem of b1 : ( ( ) ( ) 1-sorted ) ) : ( ( reflexive monotonic idempotent ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() reflexive monotonic idempotent ) MSClosureOperator of the Sorts of (ClOp->ClSys b3 : ( ( reflexive monotonic idempotent ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() reflexive monotonic idempotent ) MSClosureOperator of b2 : ( ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) ) ) : ( ( absolutely-multiplicative ) ( strict multiplicative absolutely-multiplicative properly-upper-bound ) MSClosureSystem of b1 : ( ( ) ( ) 1-sorted ) ) : ( ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) set ) ) = J : ( ( reflexive monotonic idempotent ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() reflexive monotonic idempotent ) MSClosureOperator of b2 : ( ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ManySortedSet of the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) ) ;

theorem :: CLOSURE1:40
for S being ( ( ) ( ) 1-sorted )
for D being ( ( absolutely-multiplicative ) ( multiplicative absolutely-multiplicative properly-upper-bound ) MSClosureSystem of S : ( ( ) ( ) 1-sorted ) ) holds ClOp->ClSys (ClSys->ClOp D : ( ( absolutely-multiplicative ) ( multiplicative absolutely-multiplicative properly-upper-bound ) MSClosureSystem of b1 : ( ( ) ( ) 1-sorted ) ) ) : ( ( reflexive monotonic idempotent ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total Function-yielding V25() reflexive monotonic idempotent ) MSClosureOperator of the Sorts of b2 : ( ( absolutely-multiplicative ) ( multiplicative absolutely-multiplicative properly-upper-bound ) MSClosureSystem of b1 : ( ( ) ( ) 1-sorted ) ) : ( ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) set ) ) : ( ( absolutely-multiplicative ) ( strict multiplicative absolutely-multiplicative properly-upper-bound ) MSClosureSystem of b1 : ( ( ) ( ) 1-sorted ) ) = MSClosureStr(# the Sorts of D : ( ( absolutely-multiplicative ) ( multiplicative absolutely-multiplicative properly-upper-bound ) MSClosureSystem of b1 : ( ( ) ( ) 1-sorted ) ) : ( ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total ) set ) , the Family of D : ( ( absolutely-multiplicative ) ( multiplicative absolutely-multiplicative properly-upper-bound ) MSClosureSystem of b1 : ( ( ) ( ) 1-sorted ) ) : ( ( ) ( Relation-like non-empty the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined Function-like total multiplicative absolutely-multiplicative properly-upper-bound ) MSSubsetFamily of the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) #) : ( ( strict ) ( strict multiplicative absolutely-multiplicative properly-upper-bound ) MSClosureStr over b1 : ( ( ) ( ) 1-sorted ) ) ;