:: MMLQUERY semantic presentation

begin

definition
let X be ( ( ) ( ) set ) ;
mode List of X is ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;
mode Operation of X is ( ( ) ( Relation-like X : ( ( ) ( ) 2-sorted ) -defined X : ( ( ) ( ) 2-sorted ) -valued ) Relation of ) ;
end;

definition
let x, y, R be ( ( ) ( ) set ) ;
pred x,y in R means :: MMLQUERY:def 1
[x : ( ( ) ( ) 2-sorted ) ,y : ( ( ) ( ) set ) ] : ( ( ) ( ) set ) in R : ( ( ) ( ) Element of x : ( ( ) ( ) 2-sorted ) ) ;
end;

notation
let x, y, R be ( ( ) ( ) set ) ;
antonym x,y nin R for x,y in R;
end;

theorem :: MMLQUERY:1
for R1, R2 being ( ( Relation-like ) ( Relation-like ) Relation) holds
( R1 : ( ( Relation-like ) ( Relation-like ) Relation) c= R2 : ( ( Relation-like ) ( Relation-like ) Relation) iff for z being ( ( ) ( ) set ) holds Im (R1 : ( ( Relation-like ) ( Relation-like ) Relation) ,z : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) c= Im (R2 : ( ( Relation-like ) ( Relation-like ) Relation) ,z : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

notation
let X be ( ( ) ( ) set ) ;
let O be ( ( ) ( Relation-like X : ( ( ) ( ) set ) -defined X : ( ( ) ( ) set ) -valued ) Operation of X : ( ( ) ( ) set ) ) ;
let x be ( ( ) ( ) Element of X : ( ( ) ( ) set ) ) ;
synonym x . O for Im (X,O);
end;

definition
let X be ( ( ) ( ) set ) ;
let O be ( ( ) ( Relation-like X : ( ( ) ( ) set ) -defined X : ( ( ) ( ) set ) -valued ) Operation of X : ( ( ) ( ) set ) ) ;
let x be ( ( ) ( ) Element of X : ( ( ) ( ) set ) ) ;
:: original: .
redefine func x . O -> ( ( ) ( ) List of X : ( ( ) ( ) 2-sorted ) ) ;
end;

theorem :: MMLQUERY:2
for X being ( ( ) ( ) set )
for x being ( ( ) ( ) Element of X : ( ( ) ( ) set ) )
for O being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of X : ( ( ) ( ) set ) )
for y being ( ( ) ( ) Element of X : ( ( ) ( ) set ) ) holds
( x : ( ( ) ( ) Element of b1 : ( ( ) ( ) set ) ) ,y : ( ( ) ( ) Element of b1 : ( ( ) ( ) set ) ) in O : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) iff y : ( ( ) ( ) Element of b1 : ( ( ) ( ) set ) ) in x : ( ( ) ( ) Element of b1 : ( ( ) ( ) set ) ) . O : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) ) ;

notation
let X be ( ( ) ( ) set ) ;
let O be ( ( ) ( Relation-like X : ( ( ) ( ) set ) -defined X : ( ( ) ( ) set ) -valued ) Operation of X : ( ( ) ( ) set ) ) ;
let L be ( ( ) ( ) List of X : ( ( ) ( ) set ) ) ;
synonym L | O for X .: O;
end;

definition
let X be ( ( ) ( ) set ) ;
let O be ( ( ) ( Relation-like X : ( ( ) ( ) set ) -defined X : ( ( ) ( ) set ) -valued ) Operation of X : ( ( ) ( ) set ) ) ;
let L be ( ( ) ( ) List of X : ( ( ) ( ) set ) ) ;
:: original: |
redefine func L | O -> ( ( ) ( ) List of X : ( ( ) ( ) 2-sorted ) ) equals :: MMLQUERY:def 2
 union { (x : ( ( ) ( ) Element of X : ( ( ) ( ) set ) ) . O : ( ( ) ( ) set ) ) : ( ( ) ( ) List of X : ( ( ) ( ) 2-sorted ) ) where x is ( ( ) ( ) Element of X : ( ( ) ( ) 2-sorted ) ) : x : ( ( ) ( ) Element of X : ( ( ) ( ) set ) ) in L : ( ( ) ( ) Element of X : ( ( ) ( ) 2-sorted ) ) } : ( ( ) ( ) set ) ;
func L \& O -> ( ( ) ( ) List of X : ( ( ) ( ) 2-sorted ) ) equals :: MMLQUERY:def 3
 meet { (x : ( ( ) ( ) Element of X : ( ( ) ( ) set ) ) . O : ( ( ) ( ) set ) ) : ( ( ) ( ) List of X : ( ( ) ( ) 2-sorted ) ) where x is ( ( ) ( ) Element of X : ( ( ) ( ) 2-sorted ) ) : x : ( ( ) ( ) Element of X : ( ( ) ( ) set ) ) in L : ( ( ) ( ) Element of X : ( ( ) ( ) 2-sorted ) ) } : ( ( ) ( ) set ) ;
func L WHERE O -> ( ( ) ( ) List of X : ( ( ) ( ) 2-sorted ) ) equals :: MMLQUERY:def 4
 { x : ( ( ) ( ) Element of X : ( ( ) ( ) set ) ) where x is ( ( ) ( ) Element of X : ( ( ) ( ) 2-sorted ) ) : ex y being ( ( ) ( ) Element of X : ( ( ) ( ) 2-sorted ) ) st
( x : ( ( ) ( ) Element of X : ( ( ) ( ) set ) ) ,y : ( ( ) ( ) Element of X : ( ( ) ( ) set ) ) in O : ( ( ) ( ) set ) & x : ( ( ) ( ) Element of X : ( ( ) ( ) set ) ) in L : ( ( ) ( ) Element of X : ( ( ) ( ) 2-sorted ) ) ) } ;
let O2 be ( ( ) ( Relation-like X : ( ( ) ( ) set ) -defined X : ( ( ) ( ) set ) -valued ) Operation of X : ( ( ) ( ) set ) ) ;
func L WHEREeq (O,O2) -> ( ( ) ( ) List of X : ( ( ) ( ) 2-sorted ) ) equals :: MMLQUERY:def 5
 { x : ( ( ) ( ) Element of X : ( ( ) ( ) set ) ) where x is ( ( ) ( ) Element of X : ( ( ) ( ) 2-sorted ) ) : ( card (x : ( ( ) ( ) Element of X : ( ( ) ( ) set ) ) . O : ( ( ) ( ) set ) ) : ( ( ) ( ) List of X : ( ( ) ( ) 2-sorted ) ) : ( ( cardinal ) ( epsilon-transitive epsilon-connected ordinal cardinal ) set ) = card (x : ( ( ) ( ) Element of X : ( ( ) ( ) set ) ) . O2 : ( ( ) ( Relation-like O : ( ( ) ( ) set ) -defined REAL : ( ( ) ( ) set ) -valued Function-like V21(O : ( ( ) ( ) set ) , REAL : ( ( ) ( ) set ) ) ) M10(X : ( ( ) ( ) 2-sorted ) ,O : ( ( ) ( ) set ) )) ) : ( ( ) ( ) List of X : ( ( ) ( ) 2-sorted ) ) : ( ( cardinal ) ( epsilon-transitive epsilon-connected ordinal cardinal ) set ) & x : ( ( ) ( ) Element of X : ( ( ) ( ) set ) ) in L : ( ( ) ( ) Element of X : ( ( ) ( ) 2-sorted ) ) ) } ;
func L WHEREle (O,O2) -> ( ( ) ( ) List of X : ( ( ) ( ) 2-sorted ) ) equals :: MMLQUERY:def 6
 { x : ( ( ) ( ) Element of X : ( ( ) ( ) set ) ) where x is ( ( ) ( ) Element of X : ( ( ) ( ) 2-sorted ) ) : ( card (x : ( ( ) ( ) Element of X : ( ( ) ( ) set ) ) . O : ( ( ) ( ) set ) ) : ( ( ) ( ) List of X : ( ( ) ( ) 2-sorted ) ) : ( ( cardinal ) ( epsilon-transitive epsilon-connected ordinal cardinal ) set ) c= card (x : ( ( ) ( ) Element of X : ( ( ) ( ) set ) ) . O2 : ( ( ) ( Relation-like O : ( ( ) ( ) set ) -defined REAL : ( ( ) ( ) set ) -valued Function-like V21(O : ( ( ) ( ) set ) , REAL : ( ( ) ( ) set ) ) ) M10(X : ( ( ) ( ) 2-sorted ) ,O : ( ( ) ( ) set ) )) ) : ( ( ) ( ) List of X : ( ( ) ( ) 2-sorted ) ) : ( ( cardinal ) ( epsilon-transitive epsilon-connected ordinal cardinal ) set ) & x : ( ( ) ( ) Element of X : ( ( ) ( ) set ) ) in L : ( ( ) ( ) Element of X : ( ( ) ( ) 2-sorted ) ) ) } ;
func L WHEREge (O,O2) -> ( ( ) ( ) List of X : ( ( ) ( ) 2-sorted ) ) equals :: MMLQUERY:def 7
 { x : ( ( ) ( ) Element of X : ( ( ) ( ) set ) ) where x is ( ( ) ( ) Element of X : ( ( ) ( ) 2-sorted ) ) : ( card (x : ( ( ) ( ) Element of X : ( ( ) ( ) set ) ) . O2 : ( ( ) ( Relation-like O : ( ( ) ( ) set ) -defined REAL : ( ( ) ( ) set ) -valued Function-like V21(O : ( ( ) ( ) set ) , REAL : ( ( ) ( ) set ) ) ) M10(X : ( ( ) ( ) 2-sorted ) ,O : ( ( ) ( ) set ) )) ) : ( ( ) ( ) List of X : ( ( ) ( ) 2-sorted ) ) : ( ( cardinal ) ( epsilon-transitive epsilon-connected ordinal cardinal ) set ) c= card (x : ( ( ) ( ) Element of X : ( ( ) ( ) set ) ) . O : ( ( ) ( ) set ) ) : ( ( ) ( ) List of X : ( ( ) ( ) 2-sorted ) ) : ( ( cardinal ) ( epsilon-transitive epsilon-connected ordinal cardinal ) set ) & x : ( ( ) ( ) Element of X : ( ( ) ( ) set ) ) in L : ( ( ) ( ) Element of X : ( ( ) ( ) 2-sorted ) ) ) } ;
func L WHERElt (O,O2) -> ( ( ) ( ) List of X : ( ( ) ( ) 2-sorted ) ) equals :: MMLQUERY:def 8
 { x : ( ( ) ( ) Element of X : ( ( ) ( ) set ) ) where x is ( ( ) ( ) Element of X : ( ( ) ( ) 2-sorted ) ) : ( card (x : ( ( ) ( ) Element of X : ( ( ) ( ) set ) ) . O : ( ( ) ( ) set ) ) : ( ( ) ( ) List of X : ( ( ) ( ) 2-sorted ) ) : ( ( cardinal ) ( epsilon-transitive epsilon-connected ordinal cardinal ) set ) in card (x : ( ( ) ( ) Element of X : ( ( ) ( ) set ) ) . O2 : ( ( ) ( Relation-like O : ( ( ) ( ) set ) -defined REAL : ( ( ) ( ) set ) -valued Function-like V21(O : ( ( ) ( ) set ) , REAL : ( ( ) ( ) set ) ) ) M10(X : ( ( ) ( ) 2-sorted ) ,O : ( ( ) ( ) set ) )) ) : ( ( ) ( ) List of X : ( ( ) ( ) 2-sorted ) ) : ( ( cardinal ) ( epsilon-transitive epsilon-connected ordinal cardinal ) set ) & x : ( ( ) ( ) Element of X : ( ( ) ( ) set ) ) in L : ( ( ) ( ) Element of X : ( ( ) ( ) 2-sorted ) ) ) } ;
func L WHEREgt (O,O2) -> ( ( ) ( ) List of X : ( ( ) ( ) 2-sorted ) ) equals :: MMLQUERY:def 9
 { x : ( ( ) ( ) Element of X : ( ( ) ( ) set ) ) where x is ( ( ) ( ) Element of X : ( ( ) ( ) 2-sorted ) ) : ( card (x : ( ( ) ( ) Element of X : ( ( ) ( ) set ) ) . O2 : ( ( ) ( Relation-like O : ( ( ) ( ) set ) -defined REAL : ( ( ) ( ) set ) -valued Function-like V21(O : ( ( ) ( ) set ) , REAL : ( ( ) ( ) set ) ) ) M10(X : ( ( ) ( ) 2-sorted ) ,O : ( ( ) ( ) set ) )) ) : ( ( ) ( ) List of X : ( ( ) ( ) 2-sorted ) ) : ( ( cardinal ) ( epsilon-transitive epsilon-connected ordinal cardinal ) set ) in card (x : ( ( ) ( ) Element of X : ( ( ) ( ) set ) ) . O : ( ( ) ( ) set ) ) : ( ( ) ( ) List of X : ( ( ) ( ) 2-sorted ) ) : ( ( cardinal ) ( epsilon-transitive epsilon-connected ordinal cardinal ) set ) & x : ( ( ) ( ) Element of X : ( ( ) ( ) set ) ) in L : ( ( ) ( ) Element of X : ( ( ) ( ) 2-sorted ) ) ) } ;
end;

definition
let X be ( ( ) ( ) set ) ;
let L be ( ( ) ( ) List of X : ( ( ) ( ) set ) ) ;
let O be ( ( ) ( Relation-like X : ( ( ) ( ) set ) -defined X : ( ( ) ( ) set ) -valued ) Operation of X : ( ( ) ( ) set ) ) ;
let n be ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) ;
func L WHEREeq (O,n) -> ( ( ) ( ) List of X : ( ( ) ( ) 2-sorted ) ) equals :: MMLQUERY:def 10
 { x : ( ( ) ( ) Element of X : ( ( ) ( ) set ) ) where x is ( ( ) ( ) Element of X : ( ( ) ( ) 2-sorted ) ) : ( card (x : ( ( ) ( ) Element of X : ( ( ) ( ) set ) ) . O : ( ( ) ( ) Element of X : ( ( ) ( ) 2-sorted ) ) ) : ( ( ) ( ) List of X : ( ( ) ( ) 2-sorted ) ) : ( ( cardinal ) ( epsilon-transitive epsilon-connected ordinal cardinal ) set ) = n : ( ( ) ( Relation-like L : ( ( ) ( ) set ) -defined REAL : ( ( ) ( ) set ) -valued Function-like V21(L : ( ( ) ( ) set ) , REAL : ( ( ) ( ) set ) ) ) M10(X : ( ( ) ( ) 2-sorted ) ,L : ( ( ) ( ) set ) )) & x : ( ( ) ( ) Element of X : ( ( ) ( ) set ) ) in L : ( ( ) ( ) set ) ) } ;
func L WHEREle (O,n) -> ( ( ) ( ) List of X : ( ( ) ( ) 2-sorted ) ) equals :: MMLQUERY:def 11
 { x : ( ( ) ( ) Element of X : ( ( ) ( ) set ) ) where x is ( ( ) ( ) Element of X : ( ( ) ( ) 2-sorted ) ) : ( card (x : ( ( ) ( ) Element of X : ( ( ) ( ) set ) ) . O : ( ( ) ( ) Element of X : ( ( ) ( ) 2-sorted ) ) ) : ( ( ) ( ) List of X : ( ( ) ( ) 2-sorted ) ) : ( ( cardinal ) ( epsilon-transitive epsilon-connected ordinal cardinal ) set ) c= n : ( ( ) ( Relation-like L : ( ( ) ( ) set ) -defined REAL : ( ( ) ( ) set ) -valued Function-like V21(L : ( ( ) ( ) set ) , REAL : ( ( ) ( ) set ) ) ) M10(X : ( ( ) ( ) 2-sorted ) ,L : ( ( ) ( ) set ) )) & x : ( ( ) ( ) Element of X : ( ( ) ( ) set ) ) in L : ( ( ) ( ) set ) ) } ;
func L WHEREge (O,n) -> ( ( ) ( ) List of X : ( ( ) ( ) 2-sorted ) ) equals :: MMLQUERY:def 12
 { x : ( ( ) ( ) Element of X : ( ( ) ( ) set ) ) where x is ( ( ) ( ) Element of X : ( ( ) ( ) 2-sorted ) ) : ( n : ( ( ) ( Relation-like L : ( ( ) ( ) set ) -defined REAL : ( ( ) ( ) set ) -valued Function-like V21(L : ( ( ) ( ) set ) , REAL : ( ( ) ( ) set ) ) ) M10(X : ( ( ) ( ) 2-sorted ) ,L : ( ( ) ( ) set ) )) c= card (x : ( ( ) ( ) Element of X : ( ( ) ( ) set ) ) . O : ( ( ) ( ) Element of X : ( ( ) ( ) 2-sorted ) ) ) : ( ( ) ( ) List of X : ( ( ) ( ) 2-sorted ) ) : ( ( cardinal ) ( epsilon-transitive epsilon-connected ordinal cardinal ) set ) & x : ( ( ) ( ) Element of X : ( ( ) ( ) set ) ) in L : ( ( ) ( ) set ) ) } ;
func L WHERElt (O,n) -> ( ( ) ( ) List of X : ( ( ) ( ) 2-sorted ) ) equals :: MMLQUERY:def 13
 { x : ( ( ) ( ) Element of X : ( ( ) ( ) set ) ) where x is ( ( ) ( ) Element of X : ( ( ) ( ) 2-sorted ) ) : ( card (x : ( ( ) ( ) Element of X : ( ( ) ( ) set ) ) . O : ( ( ) ( ) Element of X : ( ( ) ( ) 2-sorted ) ) ) : ( ( ) ( ) List of X : ( ( ) ( ) 2-sorted ) ) : ( ( cardinal ) ( epsilon-transitive epsilon-connected ordinal cardinal ) set ) in n : ( ( ) ( Relation-like L : ( ( ) ( ) set ) -defined REAL : ( ( ) ( ) set ) -valued Function-like V21(L : ( ( ) ( ) set ) , REAL : ( ( ) ( ) set ) ) ) M10(X : ( ( ) ( ) 2-sorted ) ,L : ( ( ) ( ) set ) )) & x : ( ( ) ( ) Element of X : ( ( ) ( ) set ) ) in L : ( ( ) ( ) set ) ) } ;
func L WHEREgt (O,n) -> ( ( ) ( ) List of X : ( ( ) ( ) 2-sorted ) ) equals :: MMLQUERY:def 14
 { x : ( ( ) ( ) Element of X : ( ( ) ( ) set ) ) where x is ( ( ) ( ) Element of X : ( ( ) ( ) 2-sorted ) ) : ( n : ( ( ) ( Relation-like L : ( ( ) ( ) set ) -defined REAL : ( ( ) ( ) set ) -valued Function-like V21(L : ( ( ) ( ) set ) , REAL : ( ( ) ( ) set ) ) ) M10(X : ( ( ) ( ) 2-sorted ) ,L : ( ( ) ( ) set ) )) in card (x : ( ( ) ( ) Element of X : ( ( ) ( ) set ) ) . O : ( ( ) ( ) Element of X : ( ( ) ( ) 2-sorted ) ) ) : ( ( ) ( ) List of X : ( ( ) ( ) 2-sorted ) ) : ( ( cardinal ) ( epsilon-transitive epsilon-connected ordinal cardinal ) set ) & x : ( ( ) ( ) Element of X : ( ( ) ( ) set ) ) in L : ( ( ) ( ) set ) ) } ;
end;

theorem :: MMLQUERY:3
for X being ( ( ) ( ) set )
for L being ( ( ) ( ) List of X : ( ( ) ( ) set ) )
for x being ( ( ) ( ) Element of X : ( ( ) ( ) set ) )
for O being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of X : ( ( ) ( ) set ) ) holds
( x : ( ( ) ( ) Element of b1 : ( ( ) ( ) set ) ) in L : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) WHERE O : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) iff ( x : ( ( ) ( ) Element of b1 : ( ( ) ( ) set ) ) in L : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) & x : ( ( ) ( ) Element of b1 : ( ( ) ( ) set ) ) . O : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) <> {} : ( ( ) ( ) set ) ) ) ;

theorem :: MMLQUERY:4
for X being ( ( ) ( ) set )
for L being ( ( ) ( ) List of X : ( ( ) ( ) set ) )
for O being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of X : ( ( ) ( ) set ) ) holds L : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) WHERE O : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) c= L : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) ;

theorem :: MMLQUERY:5
for X being ( ( ) ( ) set )
for L being ( ( ) ( ) List of X : ( ( ) ( ) set ) )
for O being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of X : ( ( ) ( ) set ) ) st L : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) c= dom O : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) holds
L : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) WHERE O : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) = L : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) ;

theorem :: MMLQUERY:6
for X being ( ( ) ( ) set )
for L1, L2 being ( ( ) ( ) List of X : ( ( ) ( ) set ) )
for O being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of X : ( ( ) ( ) set ) )
for n being ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) st n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) <> 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) & L1 : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) c= L2 : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) holds
L1 : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) WHEREge (O : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) ,n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) c= L2 : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) WHERE O : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) ;

theorem :: MMLQUERY:7
for X being ( ( ) ( ) set )
for L being ( ( ) ( ) List of X : ( ( ) ( ) set ) )
for O being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of X : ( ( ) ( ) set ) ) holds L : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) WHEREge (O : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) ,1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) = L : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) WHERE O : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) ;

theorem :: MMLQUERY:8
for X being ( ( ) ( ) set )
for L1, L2 being ( ( ) ( ) List of X : ( ( ) ( ) set ) )
for O being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of X : ( ( ) ( ) set ) )
for n being ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) st L1 : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) c= L2 : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) holds
L1 : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) WHEREgt (O : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) ,n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) c= L2 : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) WHERE O : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) ;

theorem :: MMLQUERY:9
for X being ( ( ) ( ) set )
for L being ( ( ) ( ) List of X : ( ( ) ( ) set ) )
for O being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of X : ( ( ) ( ) set ) ) holds L : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) WHEREgt (O : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) ,0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) = L : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) WHERE O : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) ;

theorem :: MMLQUERY:10
for X being ( ( ) ( ) set )
for L1, L2 being ( ( ) ( ) List of X : ( ( ) ( ) set ) )
for O being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of X : ( ( ) ( ) set ) )
for n being ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) st n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) <> 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) & L1 : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) c= L2 : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) holds
L1 : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) WHEREeq (O : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) ,n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) c= L2 : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) WHERE O : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) ;

theorem :: MMLQUERY:11
for X being ( ( ) ( ) set )
for L being ( ( ) ( ) List of X : ( ( ) ( ) set ) )
for O being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of X : ( ( ) ( ) set ) )
for n being ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) holds L : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) WHEREge (O : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) ,(n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) = L : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) WHEREgt (O : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) ,n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) ;

theorem :: MMLQUERY:12
for X being ( ( ) ( ) set )
for L being ( ( ) ( ) List of X : ( ( ) ( ) set ) )
for O being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of X : ( ( ) ( ) set ) )
for n being ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) holds L : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) WHEREle (O : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) ,n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) = L : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) WHERElt (O : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) ,(n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) ;

theorem :: MMLQUERY:13
for X being ( ( ) ( ) set )
for L1, L2 being ( ( ) ( ) List of X : ( ( ) ( ) set ) )
for O1, O2 being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of X : ( ( ) ( ) set ) )
for n, m being ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) st n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) <= m : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) & L1 : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) c= L2 : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) & O1 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) c= O2 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) holds
L1 : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) WHEREge (O1 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) ,m : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) c= L2 : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) WHEREge (O2 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) ,n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) ;

theorem :: MMLQUERY:14
for X being ( ( ) ( ) set )
for L1, L2 being ( ( ) ( ) List of X : ( ( ) ( ) set ) )
for O1, O2 being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of X : ( ( ) ( ) set ) )
for n, m being ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) st n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) <= m : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) & L1 : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) c= L2 : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) & O1 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) c= O2 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) holds
L1 : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) WHEREgt (O1 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) ,m : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) c= L2 : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) WHEREgt (O2 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) ,n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) ;

theorem :: MMLQUERY:15
for X being ( ( ) ( ) set )
for L1, L2 being ( ( ) ( ) List of X : ( ( ) ( ) set ) )
for O1, O2 being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of X : ( ( ) ( ) set ) )
for n, m being ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) st n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) <= m : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) & L1 : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) c= L2 : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) & O1 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) c= O2 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) holds
L1 : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) WHEREle (O2 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) ,n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) c= L2 : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) WHEREle (O1 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) ,m : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) ;

theorem :: MMLQUERY:16
for X being ( ( ) ( ) set )
for L1, L2 being ( ( ) ( ) List of X : ( ( ) ( ) set ) )
for O1, O2 being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of X : ( ( ) ( ) set ) )
for n, m being ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) st n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) <= m : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) & L1 : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) c= L2 : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) & O1 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) c= O2 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) holds
L1 : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) WHERElt (O2 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) ,n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) c= L2 : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) WHERElt (O1 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) ,m : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) ;

theorem :: MMLQUERY:17
for X being ( ( ) ( ) set )
for L1, L2 being ( ( ) ( ) List of X : ( ( ) ( ) set ) )
for O1, O2, O, O3 being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of X : ( ( ) ( ) set ) ) st O1 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) c= O2 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) & L1 : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) c= L2 : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) & O : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) c= O3 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) holds
L1 : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) WHEREge (O : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) ,O2 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) c= L2 : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) WHEREge (O3 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) ,O1 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) ;

theorem :: MMLQUERY:18
for X being ( ( ) ( ) set )
for L1, L2 being ( ( ) ( ) List of X : ( ( ) ( ) set ) )
for O1, O2, O, O3 being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of X : ( ( ) ( ) set ) ) st O1 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) c= O2 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) & L1 : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) c= L2 : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) & O : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) c= O3 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) holds
L1 : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) WHEREgt (O : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) ,O2 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) c= L2 : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) WHEREgt (O3 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) ,O1 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) ;

theorem :: MMLQUERY:19
for X being ( ( ) ( ) set )
for L1, L2 being ( ( ) ( ) List of X : ( ( ) ( ) set ) )
for O1, O2, O, O3 being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of X : ( ( ) ( ) set ) ) st O1 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) c= O2 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) & L1 : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) c= L2 : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) & O : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) c= O3 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) holds
L1 : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) WHEREle (O3 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) ,O1 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) c= L2 : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) WHEREle (O : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) ,O2 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) ;

theorem :: MMLQUERY:20
for X being ( ( ) ( ) set )
for L1, L2 being ( ( ) ( ) List of X : ( ( ) ( ) set ) )
for O1, O2, O, O3 being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of X : ( ( ) ( ) set ) ) st O1 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) c= O2 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) & L1 : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) c= L2 : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) & O : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) c= O3 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) holds
L1 : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) WHERElt (O3 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) ,O1 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) c= L2 : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) WHERElt (O : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) ,O2 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) ;

theorem :: MMLQUERY:21
for X being ( ( ) ( ) set )
for L being ( ( ) ( ) List of X : ( ( ) ( ) set ) )
for O, O1 being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of X : ( ( ) ( ) set ) ) holds L : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) WHEREgt (O : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) ,O1 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) c= L : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) WHERE O : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) ;

theorem :: MMLQUERY:22
for X being ( ( ) ( ) set )
for L1, L2 being ( ( ) ( ) List of X : ( ( ) ( ) set ) )
for O1, O2 being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of X : ( ( ) ( ) set ) ) st O1 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) c= O2 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) & L1 : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) c= L2 : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) holds
L1 : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) WHERE O1 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) c= L2 : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) WHERE O2 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) ;

theorem :: MMLQUERY:23
for X being ( ( ) ( ) set )
for L being ( ( ) ( ) List of X : ( ( ) ( ) set ) )
for O being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of X : ( ( ) ( ) set ) )
for a being ( ( ) ( ) Element of X : ( ( ) ( ) set ) ) holds
( a : ( ( ) ( ) Element of b1 : ( ( ) ( ) set ) ) in L : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) | O : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) iff ex b being ( ( ) ( ) Element of X : ( ( ) ( ) set ) ) st
( a : ( ( ) ( ) Element of b1 : ( ( ) ( ) set ) ) in b : ( ( ) ( ) Element of b1 : ( ( ) ( ) set ) ) . O : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) & b : ( ( ) ( ) Element of b1 : ( ( ) ( ) set ) ) in L : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) ) ) ;

notation
let X be ( ( ) ( ) set ) ;
let A, B be ( ( ) ( ) List of X : ( ( ) ( ) set ) ) ;
synonym A AND B for X /\ A;
synonym A OR B for X \/ A;
synonym A BUTNOT B for X \ A;
end;

definition
let X be ( ( ) ( ) set ) ;
let A, B be ( ( ) ( ) List of X : ( ( ) ( ) set ) ) ;
:: original: AND
redefine func A AND B -> ( ( ) ( ) List of X : ( ( ) ( ) 2-sorted ) ) ;
:: original: OR
redefine func A OR B -> ( ( ) ( ) List of X : ( ( ) ( ) 2-sorted ) ) ;
:: original: BUTNOT
redefine func A BUTNOT B -> ( ( ) ( ) List of X : ( ( ) ( ) 2-sorted ) ) ;
end;

theorem :: MMLQUERY:24
for X being ( ( ) ( ) set )
for L1, L2 being ( ( ) ( ) List of X : ( ( ) ( ) set ) )
for O being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of X : ( ( ) ( ) set ) ) st L1 : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) <> {} : ( ( ) ( ) set ) & L2 : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) <> {} : ( ( ) ( ) set ) holds
(L1 : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) OR L2 : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) \& O : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) = (L1 : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) \& O : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) AND (L2 : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) \& O : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) ;

theorem :: MMLQUERY:25
for X being ( ( ) ( ) set )
for L1, L2 being ( ( ) ( ) List of X : ( ( ) ( ) set ) )
for O1, O2 being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of X : ( ( ) ( ) set ) ) st L1 : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) c= L2 : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) & O1 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) c= O2 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) holds
L1 : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) | O1 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) c= L2 : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) | O2 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) ;

theorem :: MMLQUERY:26
for X being ( ( ) ( ) set )
for L being ( ( ) ( ) List of X : ( ( ) ( ) set ) )
for O1, O2 being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of X : ( ( ) ( ) set ) ) st O1 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) c= O2 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) holds
L : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) \& O1 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) c= L : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) \& O2 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) ;

theorem :: MMLQUERY:27
for X being ( ( ) ( ) set )
for L being ( ( ) ( ) List of X : ( ( ) ( ) set ) )
for O1, O2 being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of X : ( ( ) ( ) set ) ) holds L : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) \& (O1 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) AND O2 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) List of [:b1 : ( ( ) ( ) set ) ,b1 : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) = (L : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) \& O1 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) AND (L : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) \& O2 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) ;

theorem :: MMLQUERY:28
for X being ( ( ) ( ) set )
for L1, L2 being ( ( ) ( ) List of X : ( ( ) ( ) set ) )
for O being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of X : ( ( ) ( ) set ) ) st L1 : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) <> {} : ( ( ) ( ) set ) & L1 : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) c= L2 : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) holds
L2 : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) \& O : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) c= L1 : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) \& O : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) ;

begin

theorem :: MMLQUERY:29
for X being ( ( ) ( ) set )
for O1, O2 being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of X : ( ( ) ( ) set ) ) st ( for x being ( ( ) ( ) Element of X : ( ( ) ( ) set ) ) holds x : ( ( ) ( ) Element of b1 : ( ( ) ( ) set ) ) . O1 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) = x : ( ( ) ( ) Element of b1 : ( ( ) ( ) set ) ) . O2 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) ) holds
O1 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) = O2 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) ;

theorem :: MMLQUERY:30
for X being ( ( ) ( ) set )
for O1, O2 being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of X : ( ( ) ( ) set ) ) st ( for L being ( ( ) ( ) List of X : ( ( ) ( ) set ) ) holds L : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) | O1 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) = L : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) | O2 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) ) holds
O1 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) = O2 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) ;

definition
let X be ( ( ) ( ) set ) ;
let O be ( ( ) ( Relation-like X : ( ( ) ( ) set ) -defined X : ( ( ) ( ) set ) -valued ) Operation of X : ( ( ) ( ) set ) ) ;
func NOT O -> ( ( ) ( Relation-like X : ( ( ) ( ) 2-sorted ) -defined X : ( ( ) ( ) 2-sorted ) -valued ) Operation of X : ( ( ) ( ) 2-sorted ) ) means :: MMLQUERY:def 15
 for L being ( ( ) ( ) List of X : ( ( ) ( ) 2-sorted ) ) holds L : ( ( ) ( ) List of X : ( ( ) ( ) set ) ) | it : ( ( ) ( ) Element of X : ( ( ) ( ) 2-sorted ) ) : ( ( ) ( ) List of X : ( ( ) ( ) 2-sorted ) ) = union { (IFEQ ((x : ( ( ) ( ) Element of X : ( ( ) ( ) set ) ) . O : ( ( ) ( ) set ) ) : ( ( ) ( ) List of X : ( ( ) ( ) 2-sorted ) ) ,{} : ( ( ) ( ) set ) ,{x : ( ( ) ( ) Element of X : ( ( ) ( ) set ) ) } : ( ( ) ( non empty trivial finite 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) -element ) set ) ,{} : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) where x is ( ( ) ( ) Element of X : ( ( ) ( ) 2-sorted ) ) : x : ( ( ) ( ) Element of X : ( ( ) ( ) set ) ) in L : ( ( ) ( ) List of X : ( ( ) ( ) set ) ) } : ( ( ) ( ) set ) ;
end;

notation
let X be ( ( ) ( ) set ) ;
let O1, O2 be ( ( ) ( Relation-like X : ( ( ) ( ) set ) -defined X : ( ( ) ( ) set ) -valued ) Operation of X : ( ( ) ( ) set ) ) ;
synonym O1 AND O2 for X /\ O1;
synonym O1 OR O2 for X \/ O1;
synonym O1 BUTNOT O2 for X \ O1;
synonym O1 | O2 for X * O1;
end;

definition
let X be ( ( ) ( ) set ) ;
let O1, O2 be ( ( ) ( Relation-like X : ( ( ) ( ) set ) -defined X : ( ( ) ( ) set ) -valued ) Operation of X : ( ( ) ( ) set ) ) ;
:: original: AND
redefine func O1 AND O2 -> ( ( ) ( Relation-like X : ( ( ) ( ) 2-sorted ) -defined X : ( ( ) ( ) 2-sorted ) -valued ) Operation of X : ( ( ) ( ) 2-sorted ) ) means :: MMLQUERY:def 16
 for L being ( ( ) ( ) List of X : ( ( ) ( ) 2-sorted ) ) holds L : ( ( ) ( ) List of X : ( ( ) ( ) set ) ) | it : ( ( ) ( Relation-like O1 : ( ( ) ( ) set ) -defined REAL : ( ( ) ( ) set ) -valued Function-like V21(O1 : ( ( ) ( ) set ) , REAL : ( ( ) ( ) set ) ) ) M10(X : ( ( ) ( ) 2-sorted ) ,O1 : ( ( ) ( ) set ) )) : ( ( ) ( ) List of X : ( ( ) ( ) 2-sorted ) ) = union { ((x : ( ( ) ( ) Element of X : ( ( ) ( ) set ) ) . O1 : ( ( ) ( ) set ) ) : ( ( ) ( ) List of X : ( ( ) ( ) 2-sorted ) ) AND (x : ( ( ) ( ) Element of X : ( ( ) ( ) set ) ) . O2 : ( ( ) ( ) Element of X : ( ( ) ( ) 2-sorted ) ) ) : ( ( ) ( ) List of X : ( ( ) ( ) 2-sorted ) ) ) : ( ( ) ( ) List of X : ( ( ) ( ) 2-sorted ) ) where x is ( ( ) ( ) Element of X : ( ( ) ( ) 2-sorted ) ) : x : ( ( ) ( ) Element of X : ( ( ) ( ) set ) ) in L : ( ( ) ( ) List of X : ( ( ) ( ) set ) ) } : ( ( ) ( ) set ) ;
:: original: OR
redefine func O1 OR O2 -> ( ( ) ( Relation-like X : ( ( ) ( ) 2-sorted ) -defined X : ( ( ) ( ) 2-sorted ) -valued ) Operation of X : ( ( ) ( ) 2-sorted ) ) means :: MMLQUERY:def 17
 for L being ( ( ) ( ) List of X : ( ( ) ( ) 2-sorted ) ) holds L : ( ( ) ( ) List of X : ( ( ) ( ) set ) ) | it : ( ( ) ( Relation-like O1 : ( ( ) ( ) set ) -defined REAL : ( ( ) ( ) set ) -valued Function-like V21(O1 : ( ( ) ( ) set ) , REAL : ( ( ) ( ) set ) ) ) M10(X : ( ( ) ( ) 2-sorted ) ,O1 : ( ( ) ( ) set ) )) : ( ( ) ( ) List of X : ( ( ) ( ) 2-sorted ) ) = union { ((x : ( ( ) ( ) Element of X : ( ( ) ( ) set ) ) . O1 : ( ( ) ( ) set ) ) : ( ( ) ( ) List of X : ( ( ) ( ) 2-sorted ) ) OR (x : ( ( ) ( ) Element of X : ( ( ) ( ) set ) ) . O2 : ( ( ) ( ) Element of X : ( ( ) ( ) 2-sorted ) ) ) : ( ( ) ( ) List of X : ( ( ) ( ) 2-sorted ) ) ) : ( ( ) ( ) List of X : ( ( ) ( ) 2-sorted ) ) where x is ( ( ) ( ) Element of X : ( ( ) ( ) 2-sorted ) ) : x : ( ( ) ( ) Element of X : ( ( ) ( ) set ) ) in L : ( ( ) ( ) List of X : ( ( ) ( ) set ) ) } : ( ( ) ( ) set ) ;
:: original: BUTNOT
redefine func O1 BUTNOT O2 -> ( ( ) ( Relation-like X : ( ( ) ( ) 2-sorted ) -defined X : ( ( ) ( ) 2-sorted ) -valued ) Operation of X : ( ( ) ( ) 2-sorted ) ) means :: MMLQUERY:def 18
 for L being ( ( ) ( ) List of X : ( ( ) ( ) 2-sorted ) ) holds L : ( ( ) ( ) List of X : ( ( ) ( ) set ) ) | it : ( ( ) ( Relation-like O1 : ( ( ) ( ) set ) -defined REAL : ( ( ) ( ) set ) -valued Function-like V21(O1 : ( ( ) ( ) set ) , REAL : ( ( ) ( ) set ) ) ) M10(X : ( ( ) ( ) 2-sorted ) ,O1 : ( ( ) ( ) set ) )) : ( ( ) ( ) List of X : ( ( ) ( ) 2-sorted ) ) = union { ((x : ( ( ) ( ) Element of X : ( ( ) ( ) set ) ) . O1 : ( ( ) ( ) set ) ) : ( ( ) ( ) List of X : ( ( ) ( ) 2-sorted ) ) BUTNOT (x : ( ( ) ( ) Element of X : ( ( ) ( ) set ) ) . O2 : ( ( ) ( ) Element of X : ( ( ) ( ) 2-sorted ) ) ) : ( ( ) ( ) List of X : ( ( ) ( ) 2-sorted ) ) ) : ( ( ) ( ) List of X : ( ( ) ( ) 2-sorted ) ) where x is ( ( ) ( ) Element of X : ( ( ) ( ) 2-sorted ) ) : x : ( ( ) ( ) Element of X : ( ( ) ( ) set ) ) in L : ( ( ) ( ) List of X : ( ( ) ( ) set ) ) } : ( ( ) ( ) set ) ;
:: original: |
redefine func O1 | O2 -> ( ( ) ( Relation-like X : ( ( ) ( ) 2-sorted ) -defined X : ( ( ) ( ) 2-sorted ) -valued ) Operation of X : ( ( ) ( ) 2-sorted ) ) means :: MMLQUERY:def 19
 for L being ( ( ) ( ) List of X : ( ( ) ( ) 2-sorted ) ) holds L : ( ( ) ( ) List of X : ( ( ) ( ) set ) ) | it : ( ( ) ( Relation-like O1 : ( ( ) ( ) set ) -defined REAL : ( ( ) ( ) set ) -valued Function-like V21(O1 : ( ( ) ( ) set ) , REAL : ( ( ) ( ) set ) ) ) M10(X : ( ( ) ( ) 2-sorted ) ,O1 : ( ( ) ( ) set ) )) : ( ( ) ( ) List of X : ( ( ) ( ) 2-sorted ) ) = (L : ( ( ) ( ) List of X : ( ( ) ( ) set ) ) | O1 : ( ( ) ( ) set ) ) : ( ( ) ( ) List of X : ( ( ) ( ) 2-sorted ) ) | O2 : ( ( ) ( ) Element of X : ( ( ) ( ) 2-sorted ) ) : ( ( ) ( ) List of X : ( ( ) ( ) 2-sorted ) ) ;
func O1 \& O2 -> ( ( ) ( Relation-like X : ( ( ) ( ) 2-sorted ) -defined X : ( ( ) ( ) 2-sorted ) -valued ) Operation of X : ( ( ) ( ) 2-sorted ) ) means :: MMLQUERY:def 20
 for L being ( ( ) ( ) List of X : ( ( ) ( ) 2-sorted ) ) holds L : ( ( ) ( ) List of X : ( ( ) ( ) set ) ) | it : ( ( ) ( Relation-like O1 : ( ( ) ( ) set ) -defined REAL : ( ( ) ( ) set ) -valued Function-like V21(O1 : ( ( ) ( ) set ) , REAL : ( ( ) ( ) set ) ) ) M10(X : ( ( ) ( ) 2-sorted ) ,O1 : ( ( ) ( ) set ) )) : ( ( ) ( ) List of X : ( ( ) ( ) 2-sorted ) ) = union { ((x : ( ( ) ( ) Element of X : ( ( ) ( ) set ) ) . O1 : ( ( ) ( ) set ) ) : ( ( ) ( ) List of X : ( ( ) ( ) 2-sorted ) ) \& O2 : ( ( ) ( ) Element of X : ( ( ) ( ) 2-sorted ) ) ) : ( ( ) ( ) List of X : ( ( ) ( ) 2-sorted ) ) where x is ( ( ) ( ) Element of X : ( ( ) ( ) 2-sorted ) ) : x : ( ( ) ( ) Element of X : ( ( ) ( ) set ) ) in L : ( ( ) ( ) List of X : ( ( ) ( ) set ) ) } : ( ( ) ( ) set ) ;
end;

theorem :: MMLQUERY:31
for X being ( ( ) ( ) set )
for x being ( ( ) ( ) Element of X : ( ( ) ( ) set ) )
for O1, O2 being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of X : ( ( ) ( ) set ) ) holds x : ( ( ) ( ) Element of b1 : ( ( ) ( ) set ) ) . (O1 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) AND O2 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) = (x : ( ( ) ( ) Element of b1 : ( ( ) ( ) set ) ) . O1 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) AND (x : ( ( ) ( ) Element of b1 : ( ( ) ( ) set ) ) . O2 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) ;

theorem :: MMLQUERY:32
for X being ( ( ) ( ) set )
for x being ( ( ) ( ) Element of X : ( ( ) ( ) set ) )
for O1, O2 being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of X : ( ( ) ( ) set ) ) holds x : ( ( ) ( ) Element of b1 : ( ( ) ( ) set ) ) . (O1 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) OR O2 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) = (x : ( ( ) ( ) Element of b1 : ( ( ) ( ) set ) ) . O1 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) OR (x : ( ( ) ( ) Element of b1 : ( ( ) ( ) set ) ) . O2 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) ;

theorem :: MMLQUERY:33
for X being ( ( ) ( ) set )
for x being ( ( ) ( ) Element of X : ( ( ) ( ) set ) )
for O1, O2 being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of X : ( ( ) ( ) set ) ) holds x : ( ( ) ( ) Element of b1 : ( ( ) ( ) set ) ) . (O1 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) BUTNOT O2 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) = (x : ( ( ) ( ) Element of b1 : ( ( ) ( ) set ) ) . O1 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) BUTNOT (x : ( ( ) ( ) Element of b1 : ( ( ) ( ) set ) ) . O2 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) ;

theorem :: MMLQUERY:34
for X being ( ( ) ( ) set )
for x being ( ( ) ( ) Element of X : ( ( ) ( ) set ) )
for O1, O2 being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of X : ( ( ) ( ) set ) ) holds x : ( ( ) ( ) Element of b1 : ( ( ) ( ) set ) ) . (O1 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) | O2 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) = (x : ( ( ) ( ) Element of b1 : ( ( ) ( ) set ) ) . O1 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) | O2 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) ;

theorem :: MMLQUERY:35
for X being ( ( ) ( ) set )
for x being ( ( ) ( ) Element of X : ( ( ) ( ) set ) )
for O1, O2 being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of X : ( ( ) ( ) set ) ) holds x : ( ( ) ( ) Element of b1 : ( ( ) ( ) set ) ) . (O1 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) \& O2 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) = (x : ( ( ) ( ) Element of b1 : ( ( ) ( ) set ) ) . O1 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) \& O2 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) ;

theorem :: MMLQUERY:36
for z, s, X being ( ( ) ( ) set )
for O being ( ( ) ( Relation-like b3 : ( ( ) ( ) set ) -defined b3 : ( ( ) ( ) set ) -valued ) Operation of X : ( ( ) ( ) set ) ) holds
( [z : ( ( ) ( ) set ) ,s : ( ( ) ( ) set ) ] : ( ( ) ( ) set ) in NOT O : ( ( ) ( Relation-like b3 : ( ( ) ( ) set ) -defined b3 : ( ( ) ( ) set ) -valued ) Operation of b3 : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like b3 : ( ( ) ( ) set ) -defined b3 : ( ( ) ( ) set ) -valued ) Operation of b3 : ( ( ) ( ) set ) ) iff ( z : ( ( ) ( ) set ) = s : ( ( ) ( ) set ) & z : ( ( ) ( ) set ) in X : ( ( ) ( ) set ) & z : ( ( ) ( ) set ) nin dom O : ( ( ) ( Relation-like b3 : ( ( ) ( ) set ) -defined b3 : ( ( ) ( ) set ) -valued ) Operation of b3 : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of bool b3 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) ;

theorem :: MMLQUERY:37
for X being ( ( ) ( ) set )
for O being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of X : ( ( ) ( ) set ) ) holds NOT O : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) = id (X : ( ( ) ( ) set ) \ (dom O : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( Relation-like ) ( Relation-like ) set ) ;

theorem :: MMLQUERY:38
for X being ( ( ) ( ) set )
for O being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of X : ( ( ) ( ) set ) ) holds dom (NOT (NOT O : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = dom O : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: MMLQUERY:39
for X being ( ( ) ( ) set )
for L being ( ( ) ( ) List of X : ( ( ) ( ) set ) )
for O being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of X : ( ( ) ( ) set ) ) holds L : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) WHERE (NOT (NOT O : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) = L : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) WHERE O : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) ;

theorem :: MMLQUERY:40
for X being ( ( ) ( ) set )
for L being ( ( ) ( ) List of X : ( ( ) ( ) set ) )
for O being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of X : ( ( ) ( ) set ) ) holds L : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) WHEREeq (O : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) ,0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) = L : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) WHERE (NOT O : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) ;

theorem :: MMLQUERY:41
for X being ( ( ) ( ) set )
for O being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of X : ( ( ) ( ) set ) ) holds NOT (NOT (NOT O : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) = NOT O : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) ;

theorem :: MMLQUERY:42
for X being ( ( ) ( ) set )
for O1, O2 being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of X : ( ( ) ( ) set ) ) holds (NOT O1 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) OR (NOT O2 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) c= NOT (O1 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) AND O2 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) ;

theorem :: MMLQUERY:43
for X being ( ( ) ( ) set )
for O1, O2 being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of X : ( ( ) ( ) set ) ) holds NOT (O1 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) OR O2 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) = (NOT O1 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) AND (NOT O2 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) ;

theorem :: MMLQUERY:44
for X being ( ( ) ( ) set )
for O1, O2, O being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of X : ( ( ) ( ) set ) ) st dom O1 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = X : ( ( ) ( ) set ) & dom O2 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = X : ( ( ) ( ) set ) holds
(O1 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) OR O2 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) \& O : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) = (O1 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) \& O : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) AND (O2 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) \& O : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) ;

definition
let X be ( ( ) ( ) set ) ;
let O be ( ( ) ( Relation-like X : ( ( ) ( ) set ) -defined X : ( ( ) ( ) set ) -valued ) Operation of X : ( ( ) ( ) set ) ) ;
attr O is filtering means :: MMLQUERY:def 21
O : ( ( ) ( ) set ) c= id X : ( ( ) ( ) 2-sorted ) : ( ( Relation-like ) ( Relation-like ) set ) ;
end;

theorem :: MMLQUERY:45
for X being ( ( ) ( ) set )
for O being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of X : ( ( ) ( ) set ) ) holds
( O : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) is filtering iff O : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) = id (dom O : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( Relation-like ) ( Relation-like ) set ) ) ;

registration
let X be ( ( ) ( ) set ) ;
let O be ( ( ) ( Relation-like X : ( ( ) ( ) set ) -defined X : ( ( ) ( ) set ) -valued ) Operation of X : ( ( ) ( ) set ) ) ;
cluster NOT O : ( ( ) ( Relation-like X : ( ( ) ( ) set ) -defined X : ( ( ) ( ) set ) -valued ) Element of bool [:X : ( ( ) ( ) set ) ,X : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like X : ( ( ) ( ) set ) -defined X : ( ( ) ( ) set ) -valued ) Operation of X : ( ( ) ( ) set ) ) -> filtering ;
end;

registration
let X be ( ( ) ( ) set ) ;
cluster Relation-like X : ( ( ) ( ) set ) -defined X : ( ( ) ( ) set ) -valued filtering for ( ( ) ( ) Element of bool [:X : ( ( ) ( ) set ) ,X : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;
end;

registration
let X be ( ( ) ( ) set ) ;
let F be ( ( filtering ) ( Relation-like X : ( ( ) ( ) set ) -defined X : ( ( ) ( ) set ) -valued filtering ) Operation of X : ( ( ) ( ) set ) ) ;
let O be ( ( ) ( Relation-like X : ( ( ) ( ) set ) -defined X : ( ( ) ( ) set ) -valued ) Operation of X : ( ( ) ( ) set ) ) ;
cluster O : ( ( ) ( Relation-like X : ( ( ) ( ) set ) -defined X : ( ( ) ( ) set ) -valued ) Element of bool [:X : ( ( ) ( ) set ) ,X : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) AND : ( ( ) ( X : ( ( ) ( ) set ) -defined X : ( ( ) ( ) set ) -valued ) set ) -> filtering for ( ( ) ( Relation-like X : ( ( ) ( ) set ) -defined X : ( ( ) ( ) set ) -valued ) Operation of X : ( ( ) ( ) set ) ) ;
cluster F : ( ( filtering ) ( Relation-like X : ( ( ) ( ) set ) -defined X : ( ( ) ( ) set ) -valued filtering ) Element of bool [:X : ( ( ) ( ) set ) ,X : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) AND : ( ( ) ( X : ( ( ) ( ) set ) -defined X : ( ( ) ( ) set ) -valued ) set ) -> filtering for ( ( ) ( Relation-like X : ( ( ) ( ) set ) -defined X : ( ( ) ( ) set ) -valued ) Operation of X : ( ( ) ( ) set ) ) ;
cluster O : ( ( ) ( Relation-like X : ( ( ) ( ) set ) -defined X : ( ( ) ( ) set ) -valued ) Element of bool [:X : ( ( ) ( ) set ) ,X : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) BUTNOT : ( ( ) ( X : ( ( ) ( ) set ) -defined X : ( ( ) ( ) set ) -valued ) set ) -> filtering for ( ( ) ( Relation-like X : ( ( ) ( ) set ) -defined X : ( ( ) ( ) set ) -valued ) Operation of X : ( ( ) ( ) set ) ) ;
end;

registration
let X be ( ( ) ( ) set ) ;
let F1, F2 be ( ( filtering ) ( Relation-like X : ( ( ) ( ) set ) -defined X : ( ( ) ( ) set ) -valued filtering ) Operation of X : ( ( ) ( ) set ) ) ;
cluster F2 : ( ( filtering ) ( Relation-like X : ( ( ) ( ) set ) -defined X : ( ( ) ( ) set ) -valued filtering ) Element of bool [:X : ( ( ) ( ) set ) ,X : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) OR : ( ( ) ( X : ( ( ) ( ) set ) -defined X : ( ( ) ( ) set ) -valued ) set ) -> filtering for ( ( ) ( Relation-like X : ( ( ) ( ) set ) -defined X : ( ( ) ( ) set ) -valued ) Operation of X : ( ( ) ( ) set ) ) ;
end;

theorem :: MMLQUERY:46
for X, z being ( ( ) ( ) set )
for x being ( ( ) ( ) Element of X : ( ( ) ( ) set ) )
for F being ( ( filtering ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued filtering ) Operation of X : ( ( ) ( ) set ) ) st z : ( ( ) ( ) set ) in x : ( ( ) ( ) Element of b1 : ( ( ) ( ) set ) ) . F : ( ( filtering ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued filtering ) Operation of b1 : ( ( ) ( ) set ) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) holds
z : ( ( ) ( ) set ) = x : ( ( ) ( ) Element of b1 : ( ( ) ( ) set ) ) ;

theorem :: MMLQUERY:47
for X being ( ( ) ( ) set )
for L being ( ( ) ( ) List of X : ( ( ) ( ) set ) )
for F being ( ( filtering ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued filtering ) Operation of X : ( ( ) ( ) set ) ) holds L : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) | F : ( ( filtering ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued filtering ) Operation of b1 : ( ( ) ( ) set ) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) = L : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) WHERE F : ( ( filtering ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued filtering ) Operation of b1 : ( ( ) ( ) set ) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) ;

theorem :: MMLQUERY:48
for X being ( ( ) ( ) set )
for F being ( ( filtering ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued filtering ) Operation of X : ( ( ) ( ) set ) ) holds NOT (NOT F : ( ( filtering ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued filtering ) Operation of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued filtering ) Operation of b1 : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued filtering ) Operation of b1 : ( ( ) ( ) set ) ) = F : ( ( filtering ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued filtering ) Operation of b1 : ( ( ) ( ) set ) ) ;

theorem :: MMLQUERY:49
for X being ( ( ) ( ) set )
for F1, F2 being ( ( filtering ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued filtering ) Operation of X : ( ( ) ( ) set ) ) holds NOT (F1 : ( ( filtering ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued filtering ) Operation of b1 : ( ( ) ( ) set ) ) AND F2 : ( ( filtering ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued filtering ) Operation of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued filtering ) Operation of b1 : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued filtering ) Operation of b1 : ( ( ) ( ) set ) ) = (NOT F1 : ( ( filtering ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued filtering ) Operation of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued filtering ) Operation of b1 : ( ( ) ( ) set ) ) OR (NOT F2 : ( ( filtering ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued filtering ) Operation of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued filtering ) Operation of b1 : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued filtering ) Operation of b1 : ( ( ) ( ) set ) ) ;

theorem :: MMLQUERY:50
for X being ( ( ) ( ) set )
for O being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of X : ( ( ) ( ) set ) ) holds dom (O : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) OR (NOT O : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued filtering ) Operation of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = X : ( ( ) ( ) set ) ;

theorem :: MMLQUERY:51
for X being ( ( ) ( ) set )
for F being ( ( filtering ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued filtering ) Operation of X : ( ( ) ( ) set ) ) holds F : ( ( filtering ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued filtering ) Operation of b1 : ( ( ) ( ) set ) ) OR (NOT F : ( ( filtering ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued filtering ) Operation of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued filtering ) Operation of b1 : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued filtering ) Operation of b1 : ( ( ) ( ) set ) ) = id X : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like ) set ) ;

theorem :: MMLQUERY:52
for X being ( ( ) ( ) set )
for O being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of X : ( ( ) ( ) set ) ) holds O : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) AND (NOT O : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued filtering ) Operation of b1 : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued filtering ) Operation of b1 : ( ( ) ( ) set ) ) = {} : ( ( ) ( ) set ) ;

theorem :: MMLQUERY:53
for X being ( ( ) ( ) set )
for O1, O2 being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of X : ( ( ) ( ) set ) ) holds (O1 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) OR O2 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) AND (NOT O1 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued filtering ) Operation of b1 : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued filtering ) Operation of b1 : ( ( ) ( ) set ) ) c= O2 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Operation of b1 : ( ( ) ( ) set ) ) ;

begin

definition
let A be ( ( Relation-like Function-like FinSequence-like ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like ) FinSequence) ;
let a be ( ( ) ( ) set ) ;
func #occurrences (a,A) -> ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) equals :: MMLQUERY:def 22
 card { i : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) where i is ( ( ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( i : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) in dom A : ( ( ) ( ) set ) : ( ( ) ( ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) & a : ( ( non empty ) ( non empty ) set ) in A : ( ( ) ( ) set ) . i : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ) } : ( ( cardinal ) ( epsilon-transitive epsilon-connected ordinal cardinal ) set ) ;
end;

theorem :: MMLQUERY:54
for A being ( ( Relation-like Function-like FinSequence-like ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like ) FinSequence)
for a being ( ( ) ( ) set ) holds #occurrences (a : ( ( ) ( ) set ) ,A : ( ( Relation-like Function-like FinSequence-like ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like ) FinSequence) ) : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) <= len A : ( ( Relation-like Function-like FinSequence-like ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like ) FinSequence) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: MMLQUERY:55
for A being ( ( Relation-like Function-like FinSequence-like ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like ) FinSequence)
for a being ( ( ) ( ) set ) holds
( ( A : ( ( Relation-like Function-like FinSequence-like ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like ) FinSequence) <> {} : ( ( ) ( ) set ) & #occurrences (a : ( ( ) ( ) set ) ,A : ( ( Relation-like Function-like FinSequence-like ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like ) FinSequence) ) : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) = len A : ( ( Relation-like Function-like FinSequence-like ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like ) FinSequence) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) iff a : ( ( ) ( ) set ) in meet (rng A : ( ( Relation-like Function-like FinSequence-like ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like ) FinSequence) ) : ( ( ) ( finite ) set ) : ( ( ) ( ) set ) ) ;

definition
let A be ( ( Relation-like Function-like FinSequence-like ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like ) FinSequence) ;
func max# A -> ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) means :: MMLQUERY:def 23
( ( for a being ( ( ) ( ) set ) holds #occurrences (a : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) ,A : ( ( ) ( ) set ) ) : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) <= it : ( ( non empty ) ( non empty ) set ) ) & ( for n being ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) st ( for a being ( ( ) ( ) set ) holds #occurrences (a : ( ( ) ( ) set ) ,A : ( ( ) ( ) set ) ) : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) <= n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) ) holds
it : ( ( non empty ) ( non empty ) set ) <= n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) ) );
end;

theorem :: MMLQUERY:56
for A being ( ( Relation-like Function-like FinSequence-like ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like ) FinSequence) holds max# A : ( ( Relation-like Function-like FinSequence-like ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like ) FinSequence) : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) <= len A : ( ( Relation-like Function-like FinSequence-like ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like ) FinSequence) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: MMLQUERY:57
for A being ( ( Relation-like Function-like FinSequence-like ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like ) FinSequence)
for a being ( ( ) ( ) set ) st #occurrences (a : ( ( ) ( ) set ) ,A : ( ( Relation-like Function-like FinSequence-like ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like ) FinSequence) ) : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) = len A : ( ( Relation-like Function-like FinSequence-like ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like ) FinSequence) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) holds
max# A : ( ( Relation-like Function-like FinSequence-like ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like ) FinSequence) : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) = len A : ( ( Relation-like Function-like FinSequence-like ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined Function-like finite FinSequence-like FinSubsequence-like ) FinSequence) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ;

definition
let X be ( ( ) ( ) set ) ;
let A be ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool X : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of bool X : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ;
let n be ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) ;
func ROUGH (A,n) -> ( ( ) ( ) List of X : ( ( ) ( ) set ) ) equals :: MMLQUERY:def 24
 { x : ( ( ) ( ) Element of X : ( ( ) ( ) set ) ) where x is ( ( ) ( ) Element of X : ( ( ) ( ) set ) ) : n : ( ( filtering ) ( Relation-like X : ( ( ) ( ) set ) -defined X : ( ( ) ( ) set ) -valued filtering ) Element of bool [:X : ( ( ) ( ) set ) ,X : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) <= #occurrences (x : ( ( ) ( ) Element of X : ( ( ) ( ) set ) ) ,A : ( ( non empty ) ( non empty ) set ) ) : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) } if X : ( ( ) ( ) set ) <> {} : ( ( ) ( ) set )
;
let m be ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) ;
func ROUGH (A,n,m) -> ( ( ) ( ) List of X : ( ( ) ( ) set ) ) equals :: MMLQUERY:def 25
 { x : ( ( ) ( ) Element of X : ( ( ) ( ) set ) ) where x is ( ( ) ( ) Element of X : ( ( ) ( ) set ) ) : ( n : ( ( filtering ) ( Relation-like X : ( ( ) ( ) set ) -defined X : ( ( ) ( ) set ) -valued filtering ) Element of bool [:X : ( ( ) ( ) set ) ,X : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) <= #occurrences (x : ( ( ) ( ) Element of X : ( ( ) ( ) set ) ) ,A : ( ( non empty ) ( non empty ) set ) ) : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) & #occurrences (x : ( ( ) ( ) Element of X : ( ( ) ( ) set ) ) ,A : ( ( non empty ) ( non empty ) set ) ) : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) <= m : ( ( ) ( Relation-like A : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( ) set ) -valued Function-like V21(A : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( ) set ) ) ) M10(X : ( ( ) ( ) set ) ,A : ( ( non empty ) ( non empty ) set ) )) ) } if X : ( ( ) ( ) set ) <> {} : ( ( ) ( ) set )
;
end;

definition
let X be ( ( ) ( ) set ) ;
let A be ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool X : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of bool X : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ;
func ROUGH A -> ( ( ) ( ) List of X : ( ( ) ( ) set ) ) equals :: MMLQUERY:def 26
 ROUGH (A : ( ( non empty ) ( non empty ) set ) ,(max# A : ( ( non empty ) ( non empty ) set ) ) : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) ) : ( ( ) ( ) List of X : ( ( ) ( ) set ) ) ;
end;

theorem :: MMLQUERY:58
for X being ( ( ) ( ) set )
for n being ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat)
for A being ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of bool X : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) holds ROUGH (A : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ,n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) ,(len A : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) = ROUGH (A : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ,n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) ;

theorem :: MMLQUERY:59
for X being ( ( ) ( ) set )
for n, m being ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat)
for A being ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of bool X : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) st n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) <= m : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) holds
ROUGH (A : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ,m : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) c= ROUGH (A : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ,n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) ;

theorem :: MMLQUERY:60
for X being ( ( ) ( ) set )
for A being ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of bool X : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) )
for n1, n2, m1, m2 being ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) st n1 : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) <= m1 : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) & n2 : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) <= m2 : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) holds
ROUGH (A : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ,m1 : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) ,n2 : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) c= ROUGH (A : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ,n1 : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) ,m2 : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) ;

theorem :: MMLQUERY:61
for X being ( ( ) ( ) set )
for n, m being ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat)
for A being ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of bool X : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) holds ROUGH (A : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ,n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) ,m : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) c= ROUGH (A : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ,n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) ;

theorem :: MMLQUERY:62
for X being ( ( ) ( ) set )
for A being ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of bool X : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) st A : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) <> {} : ( ( ) ( ) set ) holds
ROUGH (A : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ,(len A : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) = meet (rng A : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( finite ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: MMLQUERY:63
for X being ( ( ) ( ) set )
for A being ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of bool X : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) holds ROUGH (A : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) = Union A : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: MMLQUERY:64
for X being ( ( ) ( ) set )
for L1, L2 being ( ( ) ( ) List of X : ( ( ) ( ) set ) ) holds ROUGH (<*L1 : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) ,L2 : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) *> : ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) -valued Function-like finite 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) -element FinSequence-like FinSubsequence-like ) FinSequence of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) = L1 : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) AND L2 : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) ;

theorem :: MMLQUERY:65
for X being ( ( ) ( ) set )
for L1, L2 being ( ( ) ( ) List of X : ( ( ) ( ) set ) ) holds ROUGH (<*L1 : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) ,L2 : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) *> : ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) -valued Function-like finite 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) -element FinSequence-like FinSubsequence-like ) FinSequence of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) = L1 : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) OR L2 : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) set ) ) ;

begin

definition
attr c1 is strict ;
struct ConstructorDB -> ( ( ) ( ) 1-sorted ) ;
aggr ConstructorDB(# carrier, Constrs, ref-operation #) -> ( ( strict ) ( strict ) ConstructorDB ) ;
sel Constrs c1 -> ( ( ) ( ) List of the carrier of c1 : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ;
sel ref-operation c1 -> ( ( ) ( Relation-like the carrier of c1 : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined the Constrs of c1 : ( ( ) ( ) set ) : ( ( ) ( ) List of the carrier of c1 : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -valued ) Relation of ,) ;
end;

definition
let X be ( ( ) ( ) 1-sorted ) ;
mode List of X is ( ( ) ( ) List of the carrier of X : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ;
mode Operation of X is ( ( ) ( Relation-like the carrier of X : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined the carrier of X : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued ) Operation of the carrier of X : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ;
end;

definition
let X be ( ( ) ( ) set ) ;
let S be ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;
let R be ( ( ) ( Relation-like X : ( ( ) ( ) set ) -defined S : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) -valued ) Relation of ,) ;
func @ R -> ( ( ) ( Relation-like X : ( ( ) ( ) set ) -defined X : ( ( ) ( ) set ) -valued ) Relation of ) equals :: MMLQUERY:def 27
R : ( ( filtering ) ( Relation-like X : ( ( ) ( ) set ) -defined X : ( ( ) ( ) set ) -valued filtering ) Element of bool [:X : ( ( ) ( ) set ) ,X : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;
end;

definition
let X be ( ( ) ( ) ConstructorDB ) ;
let a be ( ( ) ( ) Element of ( ( ) ( ) set ) ) ;
func a ref -> ( ( ) ( ) List of X : ( ( ) ( ) set ) ) equals :: MMLQUERY:def 28
a : ( ( non empty ) ( non empty ) set ) . (@ the ref-operation of X : ( ( ) ( ) set ) : ( ( ) ( Relation-like the carrier of X : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined the Constrs of X : ( ( ) ( ) set ) : ( ( ) ( ) List of the carrier of X : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -valued ) Relation of ,) ) : ( ( ) ( Relation-like the carrier of X : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined the carrier of X : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued ) Relation of ) : ( ( ) ( ) List of the carrier of X : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ;
func a occur -> ( ( ) ( ) List of X : ( ( ) ( ) set ) ) equals :: MMLQUERY:def 29
a : ( ( non empty ) ( non empty ) set ) . ((@ the ref-operation of X : ( ( ) ( ) set ) : ( ( ) ( Relation-like the carrier of X : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined the Constrs of X : ( ( ) ( ) set ) : ( ( ) ( ) List of the carrier of X : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -valued ) Relation of ,) ) : ( ( ) ( Relation-like the carrier of X : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined the carrier of X : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued ) Relation of ) ~) : ( ( ) ( Relation-like the carrier of X : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined the carrier of X : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued ) Element of bool [: the carrier of X : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of X : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) List of the carrier of X : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ;
end;

theorem :: MMLQUERY:66
for X being ( ( ) ( ) ConstructorDB )
for x, y being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds
( x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) in y : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ref : ( ( ) ( ) List of b1 : ( ( ) ( ) ConstructorDB ) ) iff y : ( ( ) ( ) Element of ( ( ) ( ) set ) ) in x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) occur : ( ( ) ( ) List of b1 : ( ( ) ( ) ConstructorDB ) ) ) ;

definition
let X be ( ( ) ( ) ConstructorDB ) ;
attr X is ref-finite means :: MMLQUERY:def 30
 for x being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ref : ( ( ) ( ) List of X : ( ( ) ( ) set ) ) is finite ;
end;

registration
cluster finite -> ref-finite for ( ( ) ( ) ConstructorDB ) ;
end;

registration
cluster non empty finite for ( ( ) ( ) ConstructorDB ) ;
end;

registration
let X be ( ( ref-finite ) ( ref-finite ) ConstructorDB ) ;
let x be ( ( ) ( ) Element of ( ( ) ( ) set ) ) ;
cluster x : ( ( ) ( ) Element of the carrier of X : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) set ) ) ref : ( ( ) ( ) List of X : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) ) -> finite ;
end;

definition
let X be ( ( ) ( ) ConstructorDB ) ;
let A be ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined the Constrs of X : ( ( ) ( ) ConstructorDB ) : ( ( ) ( ) List of the carrier of X : ( ( ) ( ) ConstructorDB ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of the Constrs of X : ( ( ) ( ) ConstructorDB ) : ( ( ) ( ) List of the carrier of X : ( ( ) ( ) ConstructorDB ) : ( ( ) ( ) set ) ) ) ;
func ATLEAST A -> ( ( ) ( ) List of X : ( ( ) ( ) set ) ) equals :: MMLQUERY:def 31
 { x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) where x is ( ( ) ( ) Element of ( ( ) ( ) set ) ) : rng A : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) Element of bool the Constrs of X : ( ( ) ( ) set ) : ( ( ) ( ) List of the carrier of X : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) c= x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ref : ( ( ) ( ) List of X : ( ( ) ( ) set ) ) } if the carrier of X : ( ( ) ( ) set ) : ( ( ) ( ) set ) <> {} : ( ( ) ( ) set )
;
func ATMOST A -> ( ( ) ( ) List of X : ( ( ) ( ) set ) ) equals :: MMLQUERY:def 32
 { x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) where x is ( ( ) ( ) Element of ( ( ) ( ) set ) ) : x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ref : ( ( ) ( ) List of X : ( ( ) ( ) set ) ) c= rng A : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) Element of bool the Constrs of X : ( ( ) ( ) set ) : ( ( ) ( ) List of the carrier of X : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) } if the carrier of X : ( ( ) ( ) set ) : ( ( ) ( ) set ) <> {} : ( ( ) ( ) set )
;
func EXACTLY A -> ( ( ) ( ) List of X : ( ( ) ( ) set ) ) equals :: MMLQUERY:def 33
 { x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) where x is ( ( ) ( ) Element of ( ( ) ( ) set ) ) : x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ref : ( ( ) ( ) List of X : ( ( ) ( ) set ) ) = rng A : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) Element of bool the Constrs of X : ( ( ) ( ) set ) : ( ( ) ( ) List of the carrier of X : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) } if the carrier of X : ( ( ) ( ) set ) : ( ( ) ( ) set ) <> {} : ( ( ) ( ) set )
;
let n be ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) ;
func ATLEAST- (A,n) -> ( ( ) ( ) List of X : ( ( ) ( ) set ) ) equals :: MMLQUERY:def 34
 { x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) where x is ( ( ) ( ) Element of ( ( ) ( ) set ) ) : card ((rng A : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the Constrs of X : ( ( ) ( ) set ) : ( ( ) ( ) List of the carrier of X : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) \ (x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ref) : ( ( ) ( ) List of X : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of bool the Constrs of X : ( ( ) ( ) set ) : ( ( ) ( ) List of the carrier of X : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Element of omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) ) <= n : ( ( filtering ) ( Relation-like X : ( ( ) ( ) set ) -defined X : ( ( ) ( ) set ) -valued filtering ) Element of bool [:X : ( ( ) ( ) set ) ,X : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) } if the carrier of X : ( ( ) ( ) set ) : ( ( ) ( ) set ) <> {} : ( ( ) ( ) set )
;
end;

definition
let X be ( ( ref-finite ) ( ref-finite ) ConstructorDB ) ;
let A be ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined the Constrs of X : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) List of the carrier of X : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of the Constrs of X : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) List of the carrier of X : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) set ) ) ) ;
let n be ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) ;
func ATMOST+ (A,n) -> ( ( ) ( ) List of X : ( ( ) ( ) set ) ) equals :: MMLQUERY:def 35
 { x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) where x is ( ( ) ( ) Element of ( ( ) ( ) set ) ) : card ((x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ref) : ( ( ) ( ) List of X : ( ( ) ( ) set ) ) \ (rng A : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the Constrs of X : ( ( ) ( ) set ) : ( ( ) ( ) List of the carrier of X : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool the carrier of X : ( ( ) ( ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Element of omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) ) <= n : ( ( filtering ) ( Relation-like X : ( ( ) ( ) set ) -defined X : ( ( ) ( ) set ) -valued filtering ) Element of bool [:X : ( ( ) ( ) set ) ,X : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) } if the carrier of X : ( ( ) ( ) set ) : ( ( ) ( ) set ) <> {} : ( ( ) ( ) set )
;
let m be ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) ;
func EXACTLY+- (A,n,m) -> ( ( ) ( ) List of X : ( ( ) ( ) set ) ) equals :: MMLQUERY:def 36
 { x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) where x is ( ( ) ( ) Element of ( ( ) ( ) set ) ) : ( card ((x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ref) : ( ( ) ( ) List of X : ( ( ) ( ) set ) ) \ (rng A : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the Constrs of X : ( ( ) ( ) set ) : ( ( ) ( ) List of the carrier of X : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool the carrier of X : ( ( ) ( ) set ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Element of omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) ) <= n : ( ( filtering ) ( Relation-like X : ( ( ) ( ) set ) -defined X : ( ( ) ( ) set ) -valued filtering ) Element of bool [:X : ( ( ) ( ) set ) ,X : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) & card ((rng A : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the Constrs of X : ( ( ) ( ) set ) : ( ( ) ( ) List of the carrier of X : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) \ (x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ref) : ( ( ) ( ) List of X : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of bool the Constrs of X : ( ( ) ( ) set ) : ( ( ) ( ) List of the carrier of X : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Element of omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) ) <= m : ( ( ) ( Relation-like A : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( ) set ) -valued Function-like V21(A : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( ) set ) ) ) M10(X : ( ( ) ( ) set ) ,A : ( ( non empty ) ( non empty ) set ) )) ) } if the carrier of X : ( ( ) ( ) set ) : ( ( ) ( ) set ) <> {} : ( ( ) ( ) set )
;
end;

theorem :: MMLQUERY:67
for X being ( ( ) ( ) ConstructorDB )
for A being ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined the Constrs of b1 : ( ( ) ( ) ConstructorDB ) : ( ( ) ( ) List of the carrier of b1 : ( ( ) ( ) ConstructorDB ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of the Constrs of X : ( ( ) ( ) ConstructorDB ) : ( ( ) ( ) List of the carrier of b1 : ( ( ) ( ) ConstructorDB ) : ( ( ) ( ) set ) ) ) holds ATLEAST- (A : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined the Constrs of b1 : ( ( ) ( ) ConstructorDB ) : ( ( ) ( ) List of the carrier of b1 : ( ( ) ( ) ConstructorDB ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of the Constrs of b1 : ( ( ) ( ) ConstructorDB ) : ( ( ) ( ) List of the carrier of b1 : ( ( ) ( ) ConstructorDB ) : ( ( ) ( ) set ) ) ) ,0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) ConstructorDB ) ) = ATLEAST A : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined the Constrs of b1 : ( ( ) ( ) ConstructorDB ) : ( ( ) ( ) List of the carrier of b1 : ( ( ) ( ) ConstructorDB ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of the Constrs of b1 : ( ( ) ( ) ConstructorDB ) : ( ( ) ( ) List of the carrier of b1 : ( ( ) ( ) ConstructorDB ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) ConstructorDB ) ) ;

theorem :: MMLQUERY:68
for Y being ( ( ref-finite ) ( ref-finite ) ConstructorDB )
for B being ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined the Constrs of b1 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) List of the carrier of b1 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of the Constrs of Y : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) List of the carrier of b1 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) set ) ) ) holds ATMOST+ (B : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined the Constrs of b1 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) List of the carrier of b1 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of the Constrs of b1 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) List of the carrier of b1 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) set ) ) ) ,0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) List of b1 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) ) = ATMOST B : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined the Constrs of b1 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) List of the carrier of b1 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of the Constrs of b1 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) List of the carrier of b1 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) List of b1 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) ) ;

theorem :: MMLQUERY:69
for Y being ( ( ref-finite ) ( ref-finite ) ConstructorDB )
for B being ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined the Constrs of b1 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) List of the carrier of b1 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of the Constrs of Y : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) List of the carrier of b1 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) set ) ) ) holds EXACTLY+- (B : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined the Constrs of b1 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) List of the carrier of b1 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of the Constrs of b1 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) List of the carrier of b1 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) set ) ) ) ,0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) List of b1 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) ) = EXACTLY B : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined the Constrs of b1 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) List of the carrier of b1 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of the Constrs of b1 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) List of the carrier of b1 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) List of b1 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) ) ;

theorem :: MMLQUERY:70
for n, m being ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat)
for X being ( ( ) ( ) ConstructorDB )
for A being ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined the Constrs of b3 : ( ( ) ( ) ConstructorDB ) : ( ( ) ( ) List of the carrier of b3 : ( ( ) ( ) ConstructorDB ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of the Constrs of X : ( ( ) ( ) ConstructorDB ) : ( ( ) ( ) List of the carrier of b3 : ( ( ) ( ) ConstructorDB ) : ( ( ) ( ) set ) ) ) st n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) <= m : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) holds
ATLEAST- (A : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined the Constrs of b3 : ( ( ) ( ) ConstructorDB ) : ( ( ) ( ) List of the carrier of b3 : ( ( ) ( ) ConstructorDB ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of the Constrs of b3 : ( ( ) ( ) ConstructorDB ) : ( ( ) ( ) List of the carrier of b3 : ( ( ) ( ) ConstructorDB ) : ( ( ) ( ) set ) ) ) ,n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) ) : ( ( ) ( ) List of b3 : ( ( ) ( ) ConstructorDB ) ) c= ATLEAST- (A : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined the Constrs of b3 : ( ( ) ( ) ConstructorDB ) : ( ( ) ( ) List of the carrier of b3 : ( ( ) ( ) ConstructorDB ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of the Constrs of b3 : ( ( ) ( ) ConstructorDB ) : ( ( ) ( ) List of the carrier of b3 : ( ( ) ( ) ConstructorDB ) : ( ( ) ( ) set ) ) ) ,m : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) ) : ( ( ) ( ) List of b3 : ( ( ) ( ) ConstructorDB ) ) ;

theorem :: MMLQUERY:71
for n, m being ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat)
for Y being ( ( ref-finite ) ( ref-finite ) ConstructorDB )
for B being ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined the Constrs of b3 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) List of the carrier of b3 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of the Constrs of Y : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) List of the carrier of b3 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) set ) ) ) st n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) <= m : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) holds
ATMOST+ (B : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined the Constrs of b3 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) List of the carrier of b3 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of the Constrs of b3 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) List of the carrier of b3 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) set ) ) ) ,n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) ) : ( ( ) ( ) List of b3 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) ) c= ATMOST+ (B : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined the Constrs of b3 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) List of the carrier of b3 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of the Constrs of b3 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) List of the carrier of b3 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) set ) ) ) ,m : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) ) : ( ( ) ( ) List of b3 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) ) ;

theorem :: MMLQUERY:72
for Y being ( ( ref-finite ) ( ref-finite ) ConstructorDB )
for B being ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined the Constrs of b1 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) List of the carrier of b1 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of the Constrs of Y : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) List of the carrier of b1 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) set ) ) )
for n1, n2, m1, m2 being ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) st n1 : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) <= m1 : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) & n2 : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) <= m2 : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) holds
EXACTLY+- (B : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined the Constrs of b1 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) List of the carrier of b1 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of the Constrs of b1 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) List of the carrier of b1 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) set ) ) ) ,n1 : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) ,n2 : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) ) : ( ( ) ( ) List of b1 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) ) c= EXACTLY+- (B : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined the Constrs of b1 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) List of the carrier of b1 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of the Constrs of b1 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) List of the carrier of b1 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) set ) ) ) ,m1 : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) ,m2 : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) ) : ( ( ) ( ) List of b1 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) ) ;

theorem :: MMLQUERY:73
for n being ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat)
for X being ( ( ) ( ) ConstructorDB )
for A being ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined the Constrs of b2 : ( ( ) ( ) ConstructorDB ) : ( ( ) ( ) List of the carrier of b2 : ( ( ) ( ) ConstructorDB ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of the Constrs of X : ( ( ) ( ) ConstructorDB ) : ( ( ) ( ) List of the carrier of b2 : ( ( ) ( ) ConstructorDB ) : ( ( ) ( ) set ) ) ) holds ATLEAST A : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined the Constrs of b2 : ( ( ) ( ) ConstructorDB ) : ( ( ) ( ) List of the carrier of b2 : ( ( ) ( ) ConstructorDB ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of the Constrs of b2 : ( ( ) ( ) ConstructorDB ) : ( ( ) ( ) List of the carrier of b2 : ( ( ) ( ) ConstructorDB ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) List of b2 : ( ( ) ( ) ConstructorDB ) ) c= ATLEAST- (A : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined the Constrs of b2 : ( ( ) ( ) ConstructorDB ) : ( ( ) ( ) List of the carrier of b2 : ( ( ) ( ) ConstructorDB ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of the Constrs of b2 : ( ( ) ( ) ConstructorDB ) : ( ( ) ( ) List of the carrier of b2 : ( ( ) ( ) ConstructorDB ) : ( ( ) ( ) set ) ) ) ,n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) ) : ( ( ) ( ) List of b2 : ( ( ) ( ) ConstructorDB ) ) ;

theorem :: MMLQUERY:74
for n being ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat)
for Y being ( ( ref-finite ) ( ref-finite ) ConstructorDB )
for B being ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined the Constrs of b2 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) List of the carrier of b2 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of the Constrs of Y : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) List of the carrier of b2 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) set ) ) ) holds ATMOST B : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined the Constrs of b2 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) List of the carrier of b2 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of the Constrs of b2 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) List of the carrier of b2 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) List of b2 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) ) c= ATMOST+ (B : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined the Constrs of b2 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) List of the carrier of b2 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of the Constrs of b2 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) List of the carrier of b2 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) set ) ) ) ,n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) ) : ( ( ) ( ) List of b2 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) ) ;

theorem :: MMLQUERY:75
for n, m being ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat)
for Y being ( ( ref-finite ) ( ref-finite ) ConstructorDB )
for B being ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined the Constrs of b3 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) List of the carrier of b3 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of the Constrs of Y : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) List of the carrier of b3 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) set ) ) ) holds EXACTLY B : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined the Constrs of b3 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) List of the carrier of b3 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of the Constrs of b3 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) List of the carrier of b3 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) List of b3 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) ) c= EXACTLY+- (B : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined the Constrs of b3 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) List of the carrier of b3 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of the Constrs of b3 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) List of the carrier of b3 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) set ) ) ) ,n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) ,m : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) ) : ( ( ) ( ) List of b3 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) ) ;

theorem :: MMLQUERY:76
for X being ( ( ) ( ) ConstructorDB )
for A being ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined the Constrs of b1 : ( ( ) ( ) ConstructorDB ) : ( ( ) ( ) List of the carrier of b1 : ( ( ) ( ) ConstructorDB ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of the Constrs of X : ( ( ) ( ) ConstructorDB ) : ( ( ) ( ) List of the carrier of b1 : ( ( ) ( ) ConstructorDB ) : ( ( ) ( ) set ) ) ) holds EXACTLY A : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined the Constrs of b1 : ( ( ) ( ) ConstructorDB ) : ( ( ) ( ) List of the carrier of b1 : ( ( ) ( ) ConstructorDB ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of the Constrs of b1 : ( ( ) ( ) ConstructorDB ) : ( ( ) ( ) List of the carrier of b1 : ( ( ) ( ) ConstructorDB ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) ConstructorDB ) ) = (ATLEAST A : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined the Constrs of b1 : ( ( ) ( ) ConstructorDB ) : ( ( ) ( ) List of the carrier of b1 : ( ( ) ( ) ConstructorDB ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of the Constrs of b1 : ( ( ) ( ) ConstructorDB ) : ( ( ) ( ) List of the carrier of b1 : ( ( ) ( ) ConstructorDB ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) ConstructorDB ) ) AND (ATMOST A : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined the Constrs of b1 : ( ( ) ( ) ConstructorDB ) : ( ( ) ( ) List of the carrier of b1 : ( ( ) ( ) ConstructorDB ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of the Constrs of b1 : ( ( ) ( ) ConstructorDB ) : ( ( ) ( ) List of the carrier of b1 : ( ( ) ( ) ConstructorDB ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) ConstructorDB ) ) : ( ( ) ( ) List of the carrier of b1 : ( ( ) ( ) ConstructorDB ) : ( ( ) ( ) set ) ) ;

theorem :: MMLQUERY:77
for n, m being ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat)
for Y being ( ( ref-finite ) ( ref-finite ) ConstructorDB )
for B being ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined the Constrs of b3 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) List of the carrier of b3 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of the Constrs of Y : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) List of the carrier of b3 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) set ) ) ) holds EXACTLY+- (B : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined the Constrs of b3 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) List of the carrier of b3 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of the Constrs of b3 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) List of the carrier of b3 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) set ) ) ) ,n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) ,m : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) ) : ( ( ) ( ) List of b3 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) ) = (ATLEAST- (B : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined the Constrs of b3 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) List of the carrier of b3 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of the Constrs of b3 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) List of the carrier of b3 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) set ) ) ) ,m : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) )) : ( ( ) ( ) List of b3 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) ) AND (ATMOST+ (B : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined the Constrs of b3 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) List of the carrier of b3 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of the Constrs of b3 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) List of the carrier of b3 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) set ) ) ) ,n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Nat) )) : ( ( ) ( ) List of b3 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) ) : ( ( ) ( ) List of the carrier of b3 : ( ( ref-finite ) ( ref-finite ) ConstructorDB ) : ( ( ) ( ) set ) ) ;

theorem :: MMLQUERY:78
for X being ( ( ) ( ) ConstructorDB )
for A being ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined the Constrs of b1 : ( ( ) ( ) ConstructorDB ) : ( ( ) ( ) List of the carrier of b1 : ( ( ) ( ) ConstructorDB ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of the Constrs of X : ( ( ) ( ) ConstructorDB ) : ( ( ) ( ) List of the carrier of b1 : ( ( ) ( ) ConstructorDB ) : ( ( ) ( ) set ) ) ) st A : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined the Constrs of b1 : ( ( ) ( ) ConstructorDB ) : ( ( ) ( ) List of the carrier of b1 : ( ( ) ( ) ConstructorDB ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of the Constrs of b1 : ( ( ) ( ) ConstructorDB ) : ( ( ) ( ) List of the carrier of b1 : ( ( ) ( ) ConstructorDB ) : ( ( ) ( ) set ) ) ) <> {} : ( ( ) ( ) set ) holds
ATLEAST A : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined the Constrs of b1 : ( ( ) ( ) ConstructorDB ) : ( ( ) ( ) List of the carrier of b1 : ( ( ) ( ) ConstructorDB ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of the Constrs of b1 : ( ( ) ( ) ConstructorDB ) : ( ( ) ( ) List of the carrier of b1 : ( ( ) ( ) ConstructorDB ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) ConstructorDB ) ) = meet { (x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) occur) : ( ( ) ( ) List of b1 : ( ( ) ( ) ConstructorDB ) ) where x is ( ( ) ( ) Element of ( ( ) ( ) set ) ) : x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) in rng A : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined the Constrs of b1 : ( ( ) ( ) ConstructorDB ) : ( ( ) ( ) List of the carrier of b1 : ( ( ) ( ) ConstructorDB ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of the Constrs of b1 : ( ( ) ( ) ConstructorDB ) : ( ( ) ( ) List of the carrier of b1 : ( ( ) ( ) ConstructorDB ) : ( ( ) ( ) set ) ) ) : ( ( ) ( finite ) Element of bool the Constrs of b1 : ( ( ) ( ) ConstructorDB ) : ( ( ) ( ) List of the carrier of b1 : ( ( ) ( ) ConstructorDB ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) } : ( ( ) ( ) set ) ;

theorem :: MMLQUERY:79
for X being ( ( ) ( ) ConstructorDB )
for A being ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined the Constrs of b1 : ( ( ) ( ) ConstructorDB ) : ( ( ) ( ) List of the carrier of b1 : ( ( ) ( ) ConstructorDB ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of the Constrs of X : ( ( ) ( ) ConstructorDB ) : ( ( ) ( ) List of the carrier of b1 : ( ( ) ( ) ConstructorDB ) : ( ( ) ( ) set ) ) )
for c1, c2 being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st A : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined the Constrs of b1 : ( ( ) ( ) ConstructorDB ) : ( ( ) ( ) List of the carrier of b1 : ( ( ) ( ) ConstructorDB ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of the Constrs of b1 : ( ( ) ( ) ConstructorDB ) : ( ( ) ( ) List of the carrier of b1 : ( ( ) ( ) ConstructorDB ) : ( ( ) ( ) set ) ) ) = <*c1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c2 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) *> : ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined Function-like finite 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) -element FinSequence-like FinSubsequence-like ) set ) holds
ATLEAST A : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined the Constrs of b1 : ( ( ) ( ) ConstructorDB ) : ( ( ) ( ) List of the carrier of b1 : ( ( ) ( ) ConstructorDB ) : ( ( ) ( ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of the Constrs of b1 : ( ( ) ( ) ConstructorDB ) : ( ( ) ( ) List of the carrier of b1 : ( ( ) ( ) ConstructorDB ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) List of b1 : ( ( ) ( ) ConstructorDB ) ) = (c1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) occur) : ( ( ) ( ) List of b1 : ( ( ) ( ) ConstructorDB ) ) AND (c2 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) occur) : ( ( ) ( ) List of b1 : ( ( ) ( ) ConstructorDB ) ) : ( ( ) ( ) List of the carrier of b1 : ( ( ) ( ) ConstructorDB ) : ( ( ) ( ) set ) ) ;