:: BVFUNC25 semantic presentation

begin

theorem :: BVFUNC25:1
for Y being ( ( non empty ) ( non empty ) set )
for a, b being ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds 'not' (a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) = a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' ('not' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ;

theorem :: BVFUNC25:2
for Y being ( ( non empty ) ( non empty ) set )
for b, a being ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds (('not' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) 'imp' ('not' a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) 'imp' (a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ;

theorem :: BVFUNC25:3
for Y being ( ( non empty ) ( non empty ) set )
for a, b being ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) = ('not' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) 'imp' ('not' a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ;

theorem :: BVFUNC25:4
for Y being ( ( non empty ) ( non empty ) set )
for a, b being ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'eqv' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) = ('not' a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) 'eqv' ('not' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ;

theorem :: BVFUNC25:5
for Y being ( ( non empty ) ( non empty ) set )
for a, b being ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) = a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' (a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ;

theorem :: BVFUNC25:6
for Y being ( ( non empty ) ( non empty ) set )
for a, b being ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'eqv' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) = (a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) 'imp' (a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ;

theorem :: BVFUNC25:7
for Y being ( ( non empty ) ( non empty ) set )
for a being ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'eqv' ('not' a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) = O_el Y : ( ( non empty ) ( non empty ) set ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ;

theorem :: BVFUNC25:8
for Y being ( ( non empty ) ( non empty ) set )
for a, b, c being ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' (b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' c : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) = b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' (a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' c : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ;

theorem :: BVFUNC25:9
for Y being ( ( non empty ) ( non empty ) set )
for a, b, c being ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' (b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' c : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) = (a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) 'imp' (a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' c : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ;

theorem :: BVFUNC25:10
for Y being ( ( non empty ) ( non empty ) set )
for a, b being ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'eqv' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) = a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'xor' ('not' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ;

theorem :: BVFUNC25:11
for Y being ( ( non empty ) ( non empty ) set )
for a, b, c being ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' (b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'xor' c : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) = (a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) 'xor' (a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' c : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ;

theorem :: BVFUNC25:12
for Y being ( ( non empty ) ( non empty ) set )
for a, b being ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'eqv' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) = 'not' (a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'xor' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ;

theorem :: BVFUNC25:13
for Y being ( ( non empty ) ( non empty ) set )
for a being ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'xor' a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) = O_el Y : ( ( non empty ) ( non empty ) set ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ;

theorem :: BVFUNC25:14
for Y being ( ( non empty ) ( non empty ) set )
for a being ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'xor' ('not' a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ;

theorem :: BVFUNC25:15
for Y being ( ( non empty ) ( non empty ) set )
for a, b being ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds (a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) 'imp' (b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) = b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ;

theorem :: BVFUNC25:16
for Y being ( ( non empty ) ( non empty ) set )
for a, b being ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds (a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) '&' (('not' a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) 'or' ('not' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) = (('not' a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) '&' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) 'or' (a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' ('not' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ;

theorem :: BVFUNC25:17
for Y being ( ( non empty ) ( non empty ) set )
for a, b being ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds (a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) 'or' (('not' a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) '&' ('not' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) = (('not' a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) 'or' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) '&' (a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' ('not' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ;

theorem :: BVFUNC25:18
for Y being ( ( non empty ) ( non empty ) set )
for a, b, c being ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'xor' (b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'xor' c : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) = (a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'xor' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) 'xor' c : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ;

theorem :: BVFUNC25:19
for Y being ( ( non empty ) ( non empty ) set )
for a, b, c being ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'eqv' (b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'eqv' c : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) = (a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'eqv' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) 'eqv' c : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ;

theorem :: BVFUNC25:20
for Y being ( ( non empty ) ( non empty ) set )
for a being ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds ('not' ('not' a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) 'imp' a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ;

theorem :: BVFUNC25:21
for Y being ( ( non empty ) ( non empty ) set )
for a, b being ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds ((a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) '&' a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) 'imp' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ;

theorem :: BVFUNC25:22
for Y being ( ( non empty ) ( non empty ) set )
for a being ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' (('not' a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) 'imp' a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ;

theorem :: BVFUNC25:23
for Y being ( ( non empty ) ( non empty ) set )
for a being ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds (('not' a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) 'imp' a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) 'eqv' a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ;

theorem :: BVFUNC25:24
for Y being ( ( non empty ) ( non empty ) set )
for a, b being ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' (a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ;

theorem :: BVFUNC25:25
for Y being ( ( non empty ) ( non empty ) set )
for a, b, c being ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds (a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) 'or' (c : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ;

theorem :: BVFUNC25:26
for Y being ( ( non empty ) ( non empty ) set )
for a, b being ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds (a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) 'or' (('not' a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) 'imp' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ;

theorem :: BVFUNC25:27
for Y being ( ( non empty ) ( non empty ) set )
for a, b being ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds (a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) 'or' (a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' ('not' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ;

theorem :: BVFUNC25:28
for Y being ( ( non empty ) ( non empty ) set )
for a, b being ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds ('not' a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) 'imp' (('not' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) 'eqv' (b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ;

theorem :: BVFUNC25:29
for Y being ( ( non empty ) ( non empty ) set )
for a, b, c being ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds (a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) 'imp' (((a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' c : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) 'imp' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) 'imp' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ;

theorem :: BVFUNC25:30
for Y being ( ( non empty ) ( non empty ) set )
for a, b being ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) = a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'eqv' (a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ;

theorem :: BVFUNC25:31
for Y being ( ( non empty ) ( non empty ) set )
for a, b being ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds
( ( a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) & b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ) iff a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) = b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) ;

theorem :: BVFUNC25:32
for Y being ( ( non empty ) ( non empty ) set )
for a being ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) = ('not' a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) 'imp' a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ;

theorem :: BVFUNC25:33
for Y being ( ( non empty ) ( non empty ) set )
for a, b being ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' ((a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) 'imp' a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ;

theorem :: BVFUNC25:34
for Y being ( ( non empty ) ( non empty ) set )
for a, b being ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) = (a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) 'imp' a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ;

theorem :: BVFUNC25:35
for Y being ( ( non empty ) ( non empty ) set )
for a, b being ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) = (b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) '&' (('not' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) 'imp' a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ;

theorem :: BVFUNC25:36
for Y being ( ( non empty ) ( non empty ) set )
for a, b being ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) = 'not' (a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' ('not' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ;

theorem :: BVFUNC25:37
for Y being ( ( non empty ) ( non empty ) set )
for a, b being ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) = ('not' a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) 'imp' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ;

theorem :: BVFUNC25:38
for Y being ( ( non empty ) ( non empty ) set )
for a, b being ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) = (a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) 'imp' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ;

theorem :: BVFUNC25:39
for Y being ( ( non empty ) ( non empty ) set )
for a, b being ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds (a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) 'imp' (a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ;

theorem :: BVFUNC25:40
for Y being ( ( non empty ) ( non empty ) set )
for a, b, c, d being ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds (a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' (b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' c : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) 'imp' ((d : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) 'imp' (a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' (d : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' c : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ;

theorem :: BVFUNC25:41
for Y being ( ( non empty ) ( non empty ) set )
for a, b, c being ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds (((a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) '&' a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) '&' c : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) 'imp' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ;

theorem :: BVFUNC25:42
for Y being ( ( non empty ) ( non empty ) set )
for b, c, a being ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds (b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' c : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) 'imp' ((a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) 'imp' c : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ;

theorem :: BVFUNC25:43
for Y being ( ( non empty ) ( non empty ) set )
for a, b, c being ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds ((a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) 'imp' c : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) 'imp' ((a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) 'imp' (c : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ;

theorem :: BVFUNC25:44
for Y being ( ( non empty ) ( non empty ) set )
for a, b, c being ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds (a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) 'imp' ((a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' c : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) 'imp' (b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' c : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ;

theorem :: BVFUNC25:45
for Y being ( ( non empty ) ( non empty ) set )
for a, b, c being ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds ((a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) '&' (a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' c : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) 'imp' (b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' c : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ;

theorem :: BVFUNC25:46
for Y being ( ( non empty ) ( non empty ) set )
for a, b, c being ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds (a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' (a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) '&' (b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' c : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) '<' c : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ;

theorem :: BVFUNC25:47
for Y being ( ( non empty ) ( non empty ) set )
for a, b, c being ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds ((a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) '&' (a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' c : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) '&' (b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' c : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) '<' ('not' a : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) 'imp' (b : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' c : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) : ( ( V12() quasi_total ) ( V12() quasi_total boolean-valued ) M2(K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ;