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