:: BVFUNC_6 semantic presentation

begin

theorem :: BVFUNC_6:1
for Y being ( ( non empty ) ( non empty ) set )
for a, b being ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' (b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' (a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_6:2
for Y being ( ( non empty ) ( non empty ) set )
for a, b being ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds (a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'imp' ((b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'imp' (a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'eqv' b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_6:3
for Y being ( ( non empty ) ( non empty ) set )
for a, b being ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds (a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'eqv' (b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_6:4
for Y being ( ( non empty ) ( non empty ) set )
for a, b, c being ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds ((a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'imp' c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'imp' (a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' (b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_6:5
for Y being ( ( non empty ) ( non empty ) set )
for a, b, c being ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds (a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' (b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'imp' ((a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'imp' c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_6:6
for Y being ( ( non empty ) ( non empty ) set )
for a, b, c being ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds (c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'imp' ((c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'imp' (c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' (a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_6:7
for Y being ( ( non empty ) ( non empty ) set )
for a, b, c being ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds ((a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'imp' c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'imp' ((a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'or' (b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_6:8
for Y being ( ( non empty ) ( non empty ) set )
for a, b, c being ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds (a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'imp' ((b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'imp' ((a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'imp' c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_6:9
for Y being ( ( non empty ) ( non empty ) set )
for a, b, c being ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds ((a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '&' (b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'imp' ((a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'imp' c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_6:10
for Y being ( ( non empty ) ( non empty ) set )
for a, b being ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds (a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' (b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' ('not' b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'imp' ('not' a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_6:11
for Y being ( ( non empty ) ( non empty ) set )
for a, b, c being ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds ((a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '&' (a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'imp' (a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' (b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_6:12
for Y being ( ( non empty ) ( non empty ) set )
for a, b, c being ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds (a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' (b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'imp' ((a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'or' (a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_6:13
for Y being ( ( non empty ) ( non empty ) set )
for a, b, c being ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds ((a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '&' (b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'imp' ((a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'or' c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_6:14
for Y being ( ( non empty ) ( non empty ) set )
for a, b, c being ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds ((a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '&' c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'imp' ((a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'or' (b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_6:15
for Y being ( ( non empty ) ( non empty ) set )
for a, b being ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) st a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) holds
a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_6:16
for Y being ( ( non empty ) ( non empty ) set )
for a, b, c being ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) st a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) holds
(a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'imp' (b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_6:17
for Y being ( ( non empty ) ( non empty ) set )
for a, b, c being ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) st a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) holds
(a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'imp' (b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_6:18
for Y being ( ( non empty ) ( non empty ) set )
for a, b, c being ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) st c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) & c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) holds
c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' (a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_6:19
for Y being ( ( non empty ) ( non empty ) set )
for a, b, c being ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) st a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) & b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) holds
(a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'imp' c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_6:20
for Y being ( ( non empty ) ( non empty ) set )
for a, b being ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) st a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) & 'not' a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) holds
b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_6:21
for Y being ( ( non empty ) ( non empty ) set )
for a, b, c, d being ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) st a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) & c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' d : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) holds
(a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'imp' (b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' d : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_6:22
for Y being ( ( non empty ) ( non empty ) set )
for a, b, c, d being ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) st a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) & c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' d : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) holds
(a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'imp' (b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' d : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_6:23
for Y being ( ( non empty ) ( non empty ) set )
for a, b being ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) st (a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' ('not' b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'imp' ('not' a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) holds
a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_6:24
for Y being ( ( non empty ) ( non empty ) set )
for a, b being ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) st a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' ('not' b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) holds
b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' ('not' a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_6:25
for Y being ( ( non empty ) ( non empty ) set )
for a, b being ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) st ('not' a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'imp' b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) holds
('not' b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'imp' a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_6:26
for Y being ( ( non empty ) ( non empty ) set )
for a, b being ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' (a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_6:27
for Y being ( ( non empty ) ( non empty ) set )
for a, b being ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds (a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'imp' (('not' a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'imp' b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_6:28
for Y being ( ( non empty ) ( non empty ) set )
for a, b being ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds ('not' (a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'imp' (('not' a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '&' ('not' b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_6:29
for Y being ( ( non empty ) ( non empty ) set )
for a, b being ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds (('not' a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '&' ('not' b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'imp' ('not' (a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_6:30
for Y being ( ( non empty ) ( non empty ) set )
for a, b being ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds ('not' (a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'imp' ('not' a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_6:31
for Y being ( ( non empty ) ( non empty ) set )
for a being ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds (a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'imp' a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_6:32
for Y being ( ( non empty ) ( non empty ) set )
for a, b being ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds (a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' ('not' a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'imp' b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_6:33
for Y being ( ( non empty ) ( non empty ) set )
for a, b being ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds (a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'imp' (('not' a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'or' b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_6:34
for Y being ( ( non empty ) ( non empty ) set )
for a, b being ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds (a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'imp' ('not' (a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' ('not' b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_6:35
for Y being ( ( non empty ) ( non empty ) set )
for a, b being ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds ('not' (a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' ('not' b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'imp' (a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_6:36
for Y being ( ( non empty ) ( non empty ) set )
for a, b being ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds ('not' (a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'imp' (('not' a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'or' ('not' b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_6:37
for Y being ( ( non empty ) ( non empty ) set )
for a, b being ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds (('not' a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'or' ('not' b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'imp' ('not' (a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_6:38
for Y being ( ( non empty ) ( non empty ) set )
for a, b being ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds (a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'imp' a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_6:39
for Y being ( ( non empty ) ( non empty ) set )
for a, b being ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds (a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'imp' (a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_6:40
for Y being ( ( non empty ) ( non empty ) set )
for a, b being ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds (a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'imp' b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_6:41
for Y being ( ( non empty ) ( non empty ) set )
for a being ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' (a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_6:42
for Y being ( ( non empty ) ( non empty ) set )
for a, b being ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds (a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'eqv' b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'imp' (a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_6:43
for Y being ( ( non empty ) ( non empty ) set )
for a, b being ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds (a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'eqv' b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'imp' (b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_6:44
for Y being ( ( non empty ) ( non empty ) set )
for a, b, c being ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds ((a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'or' c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'imp' (a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' (b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_6:45
for Y being ( ( non empty ) ( non empty ) set )
for a, b, c being ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds ((a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '&' c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'imp' (a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' (b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_6:46
for Y being ( ( non empty ) ( non empty ) set )
for a, b, c being ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds (a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' (b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'imp' ((a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'or' c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;