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 b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'or' (b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'or' (c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = ((a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '&' (b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '&' (c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

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 b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' ('not' b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'or' (b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' ('not' c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'or' (c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' ('not' a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = ((b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' ('not' a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'or' (c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' ('not' b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'or' (a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' ('not' c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

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 b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' ('not' b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '&' (b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' ('not' c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '&' (c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' ('not' a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = ((b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' ('not' a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '&' (c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' ('not' b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '&' (a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' ('not' c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

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 b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( 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(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) & c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( 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(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) holds
c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' (a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( 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(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

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 b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( 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(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) & b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( 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(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) holds
(a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'imp' c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( 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(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

for Y being ( ( non empty ) ( non empty ) set )
for a1, a2, b1, b2, c1, c2 being ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds (((a1 : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' a2 : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '&' (b1 : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' b2 : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '&' (c1 : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' c2 : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '&' ((a1 : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' b1 : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'or' c1 : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '<' (a2 : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' b2 : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'or' c2 : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

for Y being ( ( non empty ) ( non empty ) set )
for a1, a2, b1, b2 being ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds (((a1 : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' b1 : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '&' (a2 : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' b2 : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '&' (a1 : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' a2 : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '&' ('not' (b1 : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' b2 : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = (((b1 : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' a1 : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '&' (b2 : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' a2 : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '&' (b1 : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' b2 : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '&' ('not' (a1 : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' a2 : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

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 ) ) holds (a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '&' (c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' d : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = (((a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'or' (a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' d : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'or' (b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'or' (b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' d : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

for Y being ( ( non empty ) ( non empty ) set )
for a1, a2, b1, b2, b3 being ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds (a1 : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' a2 : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'or' ((b1 : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' b2 : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '&' b3 : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = (((((a1 : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' b1 : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '&' (a1 : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' b2 : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '&' (a1 : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' b3 : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '&' (a2 : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' b1 : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '&' (a2 : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' b2 : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '&' (a2 : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' b3 : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

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 ) ) holds ((a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '&' (b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '&' (c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' d : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = ((a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' ((b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '&' d : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '&' (b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' (c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' d : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '&' (c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' d : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

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 ) ) holds ((a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '&' (b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' d : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '&' (a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '<' c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' d : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

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 b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'imp' ('not' c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '&' a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '&' c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '<' 'not' b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

for Y being ( ( non empty ) ( non empty ) set )
for a1, a2, a3, b1, b2, b3 being ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds ((a1 : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' a2 : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '&' a3 : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'imp' ((b1 : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' b2 : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'or' b3 : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = ((('not' b1 : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '&' ('not' b2 : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '&' a3 : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'imp' ((('not' a1 : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'or' ('not' a2 : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'or' b3 : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

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 b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '&' (b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '&' (c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = ((a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '&' c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'or' ((('not' a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '&' ('not' b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '&' ('not' c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

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 b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '&' (b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '&' (c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '&' ((a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'or' c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = (a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '&' c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

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 b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '&' (b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '&' (c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '&' ('not' ((a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '&' c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = (((('not' a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '&' b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '&' c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'or' ((a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' ('not' b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '&' c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'or' ((a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '&' ('not' c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

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 b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '&' (b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '<' a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' (b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

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 b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '&' (b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '<' (a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'imp' c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

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 b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '&' (b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '<' a : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' (b : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' c : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() quasi_total ) ( V6() quasi_total boolean-valued ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;