:: BVFUNC_3 semantic presentation

begin

theorem :: BVFUNC_3:1
for Y being ( ( non empty ) ( non empty ) set )
for G being ( ( ) ( ) Subset of ( ( ) ( ) set ) )
for a, b being ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for PA being ( ( ) ( ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) holds a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '<' (All (a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'imp' (Ex (b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_3:2
for Y being ( ( non empty ) ( non empty ) set )
for G being ( ( ) ( ) Subset of ( ( ) ( ) set ) )
for a, b being ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for PA being ( ( ) ( ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) holds (All (a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '&' (All (b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '<' a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_3:3
for Y being ( ( non empty ) ( non empty ) set )
for G being ( ( ) ( ) Subset of ( ( ) ( ) set ) )
for a, b being ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for PA being ( ( ) ( ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) holds a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '<' (Ex (a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '&' (Ex (b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_3:4
for Y being ( ( non empty ) ( non empty ) set )
for G being ( ( ) ( ) Subset of ( ( ) ( ) set ) )
for a, b being ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for PA being ( ( ) ( ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) holds 'not' ((All (a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '&' (All (b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = (Ex (('not' a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'or' (Ex (('not' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_3:5
for Y being ( ( non empty ) ( non empty ) set )
for G being ( ( ) ( ) Subset of ( ( ) ( ) set ) )
for a, b being ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for PA being ( ( ) ( ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) holds 'not' ((Ex (a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '&' (Ex (b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = (All (('not' a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'or' (All (('not' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_3:6
for Y being ( ( non empty ) ( non empty ) set )
for G being ( ( ) ( ) Subset of ( ( ) ( ) set ) )
for a, b being ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for PA being ( ( ) ( ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) holds (All (a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'or' (All (b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '<' a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_3:7
for Y being ( ( non empty ) ( non empty ) set )
for G being ( ( ) ( ) Subset of ( ( ) ( ) set ) )
for a, b being ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for PA being ( ( ) ( ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) holds a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '<' (Ex (a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'or' (Ex (b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_3:8
for Y being ( ( non empty ) ( non empty ) set )
for G being ( ( ) ( ) Subset of ( ( ) ( ) set ) )
for a, b being ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for PA being ( ( ) ( ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) holds a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'xor' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '<' ('not' ((Ex (('not' a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'xor' (Ex (b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'or' ('not' ((Ex (a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'xor' (Ex (('not' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_3:9
for Y being ( ( non empty ) ( non empty ) set )
for G being ( ( ) ( ) Subset of ( ( ) ( ) set ) )
for a, b being ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for PA being ( ( ) ( ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) holds All ((a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '<' (All (a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'or' (Ex (b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_3:10
for Y being ( ( non empty ) ( non empty ) set )
for G being ( ( ) ( ) Subset of ( ( ) ( ) set ) )
for a, b being ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for PA being ( ( ) ( ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) holds All ((a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '<' (Ex (a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'or' (All (b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_3:11
for Y being ( ( non empty ) ( non empty ) set )
for G being ( ( ) ( ) Subset of ( ( ) ( ) set ) )
for a, b being ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for PA being ( ( ) ( ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) holds All ((a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '<' (Ex (a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'or' (Ex (b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_3:12
for Y being ( ( non empty ) ( non empty ) set )
for G being ( ( ) ( ) Subset of ( ( ) ( ) set ) )
for a, b being ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for PA being ( ( ) ( ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) holds (Ex (a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '&' (All (b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '<' Ex ((a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_3:13
for Y being ( ( non empty ) ( non empty ) set )
for G being ( ( ) ( ) Subset of ( ( ) ( ) set ) )
for a, b being ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for PA being ( ( ) ( ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) holds (All (a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '&' (Ex (b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '<' Ex ((a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_3:14
for Y being ( ( non empty ) ( non empty ) set )
for G being ( ( ) ( ) Subset of ( ( ) ( ) set ) )
for a, b being ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for PA being ( ( ) ( ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) holds All ((a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '<' (All (a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'imp' (Ex (b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_3:15
for Y being ( ( non empty ) ( non empty ) set )
for G being ( ( ) ( ) Subset of ( ( ) ( ) set ) )
for a, b being ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for PA being ( ( ) ( ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) holds All ((a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '<' (Ex (a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'imp' (Ex (b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_3:16
for Y being ( ( non empty ) ( non empty ) set )
for G being ( ( ) ( ) Subset of ( ( ) ( ) set ) )
for a, b being ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for PA being ( ( ) ( ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) holds (Ex (a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'imp' (All (b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '<' All ((a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_3:17
for Y being ( ( non empty ) ( non empty ) set )
for G being ( ( ) ( ) Subset of ( ( ) ( ) set ) )
for a, b being ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for PA being ( ( ) ( ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) holds a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '<' a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' (Ex (b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_3:18
for Y being ( ( non empty ) ( non empty ) set )
for G being ( ( ) ( ) Subset of ( ( ) ( ) set ) )
for a, b being ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for PA being ( ( ) ( ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) holds a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '<' (All (a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'imp' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_3:19
for Y being ( ( non empty ) ( non empty ) set )
for G being ( ( ) ( ) Subset of ( ( ) ( ) set ) )
for a, b being ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for PA being ( ( ) ( ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) holds Ex ((a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '<' (All (a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'imp' (Ex (b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_3:20
for Y being ( ( non empty ) ( non empty ) set )
for G being ( ( ) ( ) Subset of ( ( ) ( ) set ) )
for a, b being ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for PA being ( ( ) ( ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) holds All (a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '<' (Ex (b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'imp' (Ex ((a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_3:21
for Y being ( ( non empty ) ( non empty ) set )
for G being ( ( ) ( ) Subset of ( ( ) ( ) set ) )
for u, a being ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for PA being ( ( ) ( ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) st u : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) is_independent_of PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) holds
Ex ((u : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '<' u : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' (Ex (a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_3:22
for Y being ( ( non empty ) ( non empty ) set )
for G being ( ( ) ( ) Subset of ( ( ) ( ) set ) )
for u, a being ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for PA being ( ( ) ( ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) st u : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) is_independent_of PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) holds
Ex ((a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' u : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '<' (All (a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'imp' u : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_3:23
for Y being ( ( non empty ) ( non empty ) set )
for G being ( ( ) ( ) Subset of ( ( ) ( ) set ) )
for a, b being ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for PA being ( ( ) ( ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) holds (All (a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'imp' (Ex (b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = Ex ((a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_3:24
for Y being ( ( non empty ) ( non empty ) set )
for G being ( ( ) ( ) Subset of ( ( ) ( ) set ) )
for a, b being ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for PA being ( ( ) ( ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) holds (All (a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'imp' (All (b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '<' (All (a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'imp' (Ex (b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_3:25
for Y being ( ( non empty ) ( non empty ) set )
for G being ( ( ) ( ) Subset of ( ( ) ( ) set ) )
for a, b being ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for PA being ( ( ) ( ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) holds (Ex (a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'imp' (Ex (b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '<' (All (a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'imp' (Ex (b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_3:26
for Y being ( ( non empty ) ( non empty ) set )
for G being ( ( ) ( ) Subset of ( ( ) ( ) set ) )
for a, b being ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for PA being ( ( ) ( ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) holds All ((a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = All ((('not' a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'or' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_3:27
for Y being ( ( non empty ) ( non empty ) set )
for G being ( ( ) ( ) Subset of ( ( ) ( ) set ) )
for a, b being ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for PA being ( ( ) ( ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) holds All ((a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = 'not' (Ex ((a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' ('not' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_3:28
for Y being ( ( non empty ) ( non empty ) set )
for G being ( ( ) ( ) Subset of ( ( ) ( ) set ) )
for a, b being ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for PA being ( ( ) ( ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) holds Ex (a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '<' 'not' ((All ((a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '&' (All ((a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' ('not' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_3:29
for Y being ( ( non empty ) ( non empty ) set )
for G being ( ( ) ( ) Subset of ( ( ) ( ) set ) )
for a, b being ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for PA being ( ( ) ( ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) holds Ex (a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '<' 'not' (('not' (Ex ((a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '&' ('not' (Ex ((a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' ('not' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_3:30
for Y being ( ( non empty ) ( non empty ) set )
for G being ( ( ) ( ) Subset of ( ( ) ( ) set ) )
for a, b being ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for PA being ( ( ) ( ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) holds (Ex (a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '&' (All ((a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '<' Ex ((a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_3:31
for Y being ( ( non empty ) ( non empty ) set )
for G being ( ( ) ( ) Subset of ( ( ) ( ) set ) )
for a, b being ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for PA being ( ( ) ( ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) holds (Ex (a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '&' ('not' (Ex ((a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '<' 'not' (All ((a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_3:32
for Y being ( ( non empty ) ( non empty ) set )
for G being ( ( ) ( ) Subset of ( ( ) ( ) set ) )
for a, c, b being ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for PA being ( ( ) ( ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) holds (All ((a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' c : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '&' (All ((c : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '<' All ((a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_3:33
for Y being ( ( non empty ) ( non empty ) set )
for G being ( ( ) ( ) Subset of ( ( ) ( ) set ) )
for c, b, a being ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for PA being ( ( ) ( ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) holds (All ((c : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '&' (Ex ((a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' c : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '<' Ex ((a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_3:34
for Y being ( ( non empty ) ( non empty ) set )
for G being ( ( ) ( ) Subset of ( ( ) ( ) set ) )
for b, c, a being ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for PA being ( ( ) ( ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) holds (All ((b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' ('not' c : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '&' (All ((a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' c : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '<' All ((a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' ('not' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_3:35
for Y being ( ( non empty ) ( non empty ) set )
for G being ( ( ) ( ) Subset of ( ( ) ( ) set ) )
for b, c, a being ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for PA being ( ( ) ( ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) holds (All ((b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' c : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '&' (All ((a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' ('not' c : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '<' All ((a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' ('not' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_3:36
for Y being ( ( non empty ) ( non empty ) set )
for G being ( ( ) ( ) Subset of ( ( ) ( ) set ) )
for b, c, a being ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for PA being ( ( ) ( ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) holds (All ((b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' ('not' c : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '&' (Ex ((a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' c : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '<' Ex ((a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' ('not' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_3:37
for Y being ( ( non empty ) ( non empty ) set )
for G being ( ( ) ( ) Subset of ( ( ) ( ) set ) )
for b, c, a being ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for PA being ( ( ) ( ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) holds (All ((b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' c : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '&' (Ex ((a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' ('not' c : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '<' Ex ((a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' ('not' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_3:38
for Y being ( ( non empty ) ( non empty ) set )
for G being ( ( ) ( ) Subset of ( ( ) ( ) set ) )
for c, b, a being ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for PA being ( ( ) ( ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) holds ((Ex (c : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '&' (All ((c : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '&' (All ((c : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '<' Ex ((a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_3:39
for Y being ( ( non empty ) ( non empty ) set )
for G being ( ( ) ( ) Subset of ( ( ) ( ) set ) )
for b, c, a being ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for PA being ( ( ) ( ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) holds (All ((b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' c : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '&' (All ((c : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' ('not' a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '<' All ((a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' ('not' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_3:40
for Y being ( ( non empty ) ( non empty ) set )
for G being ( ( ) ( ) Subset of ( ( ) ( ) set ) )
for b, c, a being ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for PA being ( ( ) ( ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) holds ((Ex (b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '&' (All ((b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' c : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '&' (All ((c : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '<' Ex ((a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_3:41
for Y being ( ( non empty ) ( non empty ) set )
for G being ( ( ) ( ) Subset of ( ( ) ( ) set ) )
for c, b, a being ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for PA being ( ( ) ( ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) holds ((Ex (c : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '&' (All ((b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' ('not' c : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '&' (All ((c : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '<' Ex ((a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' ('not' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;