begin
begin
theorem
for
Y being ( ( non
empty ) ( non
empty )
set )
for
a,
b being ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Function of
Y : ( ( non
empty ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
for
G being ( ( ) ( )
Subset of ( ( ) ( )
set ) )
for
A being ( ( ) ( non
empty with_non-empty_elements )
a_partition of
Y : ( ( non
empty ) ( non
empty )
set ) ) st
a : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Function of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
'<' b : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Function of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) ) holds
All (
a : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Function of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) ) ,
A : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
'<' Ex (
b : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Function of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) ) ,
A : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ;
theorem
for
Y being ( ( non
empty ) ( non
empty )
set )
for
a being ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Function of
Y : ( ( non
empty ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
for
G being ( ( ) ( )
Subset of ( ( ) ( )
set ) )
for
A,
B being ( ( ) ( non
empty with_non-empty_elements )
a_partition of
Y : ( ( non
empty ) ( non
empty )
set ) ) st
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) is
independent holds
All (
(All (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
B : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
'<' Ex (
(All (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
A : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ;
theorem
for
Y being ( ( non
empty ) ( non
empty )
set )
for
a being ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Function of
Y : ( ( non
empty ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
for
G being ( ( ) ( )
Subset of ( ( ) ( )
set ) )
for
A,
B being ( ( ) ( non
empty with_non-empty_elements )
a_partition of
Y : ( ( non
empty ) ( non
empty )
set ) ) holds
All (
(All (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
B : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
'<' Ex (
(Ex (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
A : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ;
theorem
for
Y being ( ( non
empty ) ( non
empty )
set )
for
a being ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Function of
Y : ( ( non
empty ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
for
G being ( ( ) ( )
Subset of ( ( ) ( )
set ) )
for
A,
B being ( ( ) ( non
empty with_non-empty_elements )
a_partition of
Y : ( ( non
empty ) ( non
empty )
set ) ) st
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) is
independent holds
All (
(All (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
B : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
'<' All (
(Ex (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
A : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ;
theorem
for
Y being ( ( non
empty ) ( non
empty )
set )
for
a being ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Function of
Y : ( ( non
empty ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
for
G being ( ( ) ( )
Subset of ( ( ) ( )
set ) )
for
A,
B being ( ( ) ( non
empty with_non-empty_elements )
a_partition of
Y : ( ( non
empty ) ( non
empty )
set ) ) holds
All (
(Ex (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
B : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
'<' Ex (
(Ex (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
A : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ;
theorem
for
Y being ( ( non
empty ) ( non
empty )
set )
for
a being ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Function of
Y : ( ( non
empty ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
for
G being ( ( ) ( )
Subset of ( ( ) ( )
set ) )
for
A,
B being ( ( ) ( non
empty with_non-empty_elements )
a_partition of
Y : ( ( non
empty ) ( non
empty )
set ) ) holds
'not' (Ex ((All (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
'<' Ex (
(Ex (('not' a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
A : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ;
theorem
for
Y being ( ( non
empty ) ( non
empty )
set )
for
a being ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Function of
Y : ( ( non
empty ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
for
G being ( ( ) ( )
Subset of ( ( ) ( )
set ) )
for
A,
B being ( ( ) ( non
empty with_non-empty_elements )
a_partition of
Y : ( ( non
empty ) ( non
empty )
set ) ) st
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) is
independent holds
Ex (
('not' (All (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
B : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
'<' Ex (
(Ex (('not' a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
A : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ;
theorem
for
Y being ( ( non
empty ) ( non
empty )
set )
for
a being ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Function of
Y : ( ( non
empty ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
for
G being ( ( ) ( )
Subset of ( ( ) ( )
set ) )
for
A,
B being ( ( ) ( non
empty with_non-empty_elements )
a_partition of
Y : ( ( non
empty ) ( non
empty )
set ) ) st
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) is
independent holds
'not' (All ((All (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
= Ex (
('not' (All (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
A : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ;
theorem
for
Y being ( ( non
empty ) ( non
empty )
set )
for
a being ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Function of
Y : ( ( non
empty ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
for
G being ( ( ) ( )
Subset of ( ( ) ( )
set ) )
for
A,
B being ( ( ) ( non
empty with_non-empty_elements )
a_partition of
Y : ( ( non
empty ) ( non
empty )
set ) ) st
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) is
independent holds
All (
('not' (All (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
B : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
'<' Ex (
(Ex (('not' a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
A : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ;
theorem
for
Y being ( ( non
empty ) ( non
empty )
set )
for
a being ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Function of
Y : ( ( non
empty ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
for
G being ( ( ) ( )
Subset of ( ( ) ( )
set ) )
for
A,
B being ( ( ) ( non
empty with_non-empty_elements )
a_partition of
Y : ( ( non
empty ) ( non
empty )
set ) ) st
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) is
independent holds
'not' (All ((All (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
= Ex (
(Ex (('not' a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
A : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ;
theorem
for
Y being ( ( non
empty ) ( non
empty )
set )
for
a being ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Function of
Y : ( ( non
empty ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
for
G being ( ( ) ( )
Subset of ( ( ) ( )
set ) )
for
A,
B being ( ( ) ( non
empty with_non-empty_elements )
a_partition of
Y : ( ( non
empty ) ( non
empty )
set ) ) st
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) is
independent holds
'not' (All ((All (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
'<' Ex (
(Ex (('not' a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
B : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ;
theorem
for
Y being ( ( non
empty ) ( non
empty )
set )
for
a being ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Function of
Y : ( ( non
empty ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
for
G being ( ( ) ( )
Subset of ( ( ) ( )
set ) )
for
A,
B being ( ( ) ( non
empty with_non-empty_elements )
a_partition of
Y : ( ( non
empty ) ( non
empty )
set ) ) holds
'not' (All ((Ex (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
= Ex (
(All (('not' a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
B : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ;
theorem
for
Y being ( ( non
empty ) ( non
empty )
set )
for
a being ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Function of
Y : ( ( non
empty ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
for
G being ( ( ) ( )
Subset of ( ( ) ( )
set ) )
for
A,
B being ( ( ) ( non
empty with_non-empty_elements )
a_partition of
Y : ( ( non
empty ) ( non
empty )
set ) ) holds
'not' (Ex ((All (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
= All (
(Ex (('not' a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
B : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ;
theorem
for
Y being ( ( non
empty ) ( non
empty )
set )
for
a being ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Function of
Y : ( ( non
empty ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
for
G being ( ( ) ( )
Subset of ( ( ) ( )
set ) )
for
A,
B being ( ( ) ( non
empty with_non-empty_elements )
a_partition of
Y : ( ( non
empty ) ( non
empty )
set ) ) holds
'not' (All ((All (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
= Ex (
(Ex (('not' a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
B : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ;
theorem
for
Y being ( ( non
empty ) ( non
empty )
set )
for
a being ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Function of
Y : ( ( non
empty ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
for
G being ( ( ) ( )
Subset of ( ( ) ( )
set ) )
for
A,
B being ( ( ) ( non
empty with_non-empty_elements )
a_partition of
Y : ( ( non
empty ) ( non
empty )
set ) ) st
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) is
independent holds
Ex (
(All (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
B : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
'<' Ex (
(Ex (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
A : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ;
theorem
for
Y being ( ( non
empty ) ( non
empty )
set )
for
a being ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Function of
Y : ( ( non
empty ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
for
G being ( ( ) ( )
Subset of ( ( ) ( )
set ) )
for
A,
B being ( ( ) ( non
empty with_non-empty_elements )
a_partition of
Y : ( ( non
empty ) ( non
empty )
set ) ) holds
All (
(All (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
B : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
'<' All (
(Ex (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
B : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ;
theorem
for
Y being ( ( non
empty ) ( non
empty )
set )
for
a being ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Function of
Y : ( ( non
empty ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
for
G being ( ( ) ( )
Subset of ( ( ) ( )
set ) )
for
A,
B being ( ( ) ( non
empty with_non-empty_elements )
a_partition of
Y : ( ( non
empty ) ( non
empty )
set ) ) holds
All (
(All (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
B : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
'<' Ex (
(Ex (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
B : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ;
theorem
for
Y being ( ( non
empty ) ( non
empty )
set )
for
a being ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Function of
Y : ( ( non
empty ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
for
G being ( ( ) ( )
Subset of ( ( ) ( )
set ) )
for
A,
B being ( ( ) ( non
empty with_non-empty_elements )
a_partition of
Y : ( ( non
empty ) ( non
empty )
set ) ) holds
Ex (
(All (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
B : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
'<' Ex (
(Ex (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
B : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ;
theorem
for
Y being ( ( non
empty ) ( non
empty )
set )
for
a being ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Function of
Y : ( ( non
empty ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
for
G being ( ( ) ( )
Subset of ( ( ) ( )
set ) )
for
A,
B being ( ( ) ( non
empty with_non-empty_elements )
a_partition of
Y : ( ( non
empty ) ( non
empty )
set ) ) st
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) is
independent holds
All (
('not' (All (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
B : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
'<' 'not' (All ((All (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ;
theorem
for
Y being ( ( non
empty ) ( non
empty )
set )
for
a being ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Function of
Y : ( ( non
empty ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
for
G being ( ( ) ( )
Subset of ( ( ) ( )
set ) )
for
A,
B being ( ( ) ( non
empty with_non-empty_elements )
a_partition of
Y : ( ( non
empty ) ( non
empty )
set ) ) holds
All (
(All (('not' a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
B : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
'<' 'not' (All ((All (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ;
theorem
for
Y being ( ( non
empty ) ( non
empty )
set )
for
a being ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Function of
Y : ( ( non
empty ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
for
G being ( ( ) ( )
Subset of ( ( ) ( )
set ) )
for
A,
B being ( ( ) ( non
empty with_non-empty_elements )
a_partition of
Y : ( ( non
empty ) ( non
empty )
set ) ) holds
All (
('not' (Ex (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
B : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
'<' 'not' (All ((All (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ;
theorem
for
Y being ( ( non
empty ) ( non
empty )
set )
for
a being ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Function of
Y : ( ( non
empty ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
for
G being ( ( ) ( )
Subset of ( ( ) ( )
set ) )
for
A,
B being ( ( ) ( non
empty with_non-empty_elements )
a_partition of
Y : ( ( non
empty ) ( non
empty )
set ) ) st
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) is
independent holds
All (
(Ex (('not' a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
B : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
'<' 'not' (All ((All (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ;
theorem
for
Y being ( ( non
empty ) ( non
empty )
set )
for
a being ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Function of
Y : ( ( non
empty ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
for
G being ( ( ) ( )
Subset of ( ( ) ( )
set ) )
for
A,
B being ( ( ) ( non
empty with_non-empty_elements )
a_partition of
Y : ( ( non
empty ) ( non
empty )
set ) ) st
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) is
independent holds
Ex (
(All (('not' a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
B : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
'<' 'not' (All ((All (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ;
theorem
for
Y being ( ( non
empty ) ( non
empty )
set )
for
a being ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Function of
Y : ( ( non
empty ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
for
G being ( ( ) ( )
Subset of ( ( ) ( )
set ) )
for
A,
B being ( ( ) ( non
empty with_non-empty_elements )
a_partition of
Y : ( ( non
empty ) ( non
empty )
set ) ) st
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) is
independent holds
Ex (
('not' (Ex (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
B : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
'<' 'not' (All ((All (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ;
theorem
for
Y being ( ( non
empty ) ( non
empty )
set )
for
a being ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Function of
Y : ( ( non
empty ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
for
G being ( ( ) ( )
Subset of ( ( ) ( )
set ) )
for
A,
B being ( ( ) ( non
empty with_non-empty_elements )
a_partition of
Y : ( ( non
empty ) ( non
empty )
set ) ) st
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) is
independent holds
'not' (All ((Ex (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
'<' 'not' (Ex ((All (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ;
theorem
for
Y being ( ( non
empty ) ( non
empty )
set )
for
a being ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Function of
Y : ( ( non
empty ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
for
G being ( ( ) ( )
Subset of ( ( ) ( )
set ) )
for
A,
B being ( ( ) ( non
empty with_non-empty_elements )
a_partition of
Y : ( ( non
empty ) ( non
empty )
set ) ) st
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) is
independent holds
'not' (Ex ((Ex (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
'<' 'not' (Ex ((All (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ;
theorem
for
Y being ( ( non
empty ) ( non
empty )
set )
for
a being ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Function of
Y : ( ( non
empty ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
for
G being ( ( ) ( )
Subset of ( ( ) ( )
set ) )
for
A,
B being ( ( ) ( non
empty with_non-empty_elements )
a_partition of
Y : ( ( non
empty ) ( non
empty )
set ) ) holds
'not' (Ex ((Ex (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
'<' 'not' (All ((Ex (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ;
theorem
for
Y being ( ( non
empty ) ( non
empty )
set )
for
a being ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Function of
Y : ( ( non
empty ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
for
G being ( ( ) ( )
Subset of ( ( ) ( )
set ) )
for
A,
B being ( ( ) ( non
empty with_non-empty_elements )
a_partition of
Y : ( ( non
empty ) ( non
empty )
set ) ) st
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) is
independent holds
'not' (Ex ((All (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
'<' 'not' (All ((All (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ;
theorem
for
Y being ( ( non
empty ) ( non
empty )
set )
for
a being ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Function of
Y : ( ( non
empty ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
for
G being ( ( ) ( )
Subset of ( ( ) ( )
set ) )
for
A,
B being ( ( ) ( non
empty with_non-empty_elements )
a_partition of
Y : ( ( non
empty ) ( non
empty )
set ) ) st
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) is
independent holds
'not' (All ((Ex (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
'<' 'not' (All ((All (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ;
theorem
for
Y being ( ( non
empty ) ( non
empty )
set )
for
a being ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Function of
Y : ( ( non
empty ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
for
G being ( ( ) ( )
Subset of ( ( ) ( )
set ) )
for
A,
B being ( ( ) ( non
empty with_non-empty_elements )
a_partition of
Y : ( ( non
empty ) ( non
empty )
set ) ) holds
'not' (Ex ((Ex (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
'<' 'not' (All ((All (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ;
theorem
for
Y being ( ( non
empty ) ( non
empty )
set )
for
a being ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Function of
Y : ( ( non
empty ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
for
G being ( ( ) ( )
Subset of ( ( ) ( )
set ) )
for
A,
B being ( ( ) ( non
empty with_non-empty_elements )
a_partition of
Y : ( ( non
empty ) ( non
empty )
set ) ) st
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) is
independent holds
'not' (Ex ((All (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
'<' Ex (
('not' (All (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
A : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ;
theorem
for
Y being ( ( non
empty ) ( non
empty )
set )
for
a being ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Function of
Y : ( ( non
empty ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
for
G being ( ( ) ( )
Subset of ( ( ) ( )
set ) )
for
A,
B being ( ( ) ( non
empty with_non-empty_elements )
a_partition of
Y : ( ( non
empty ) ( non
empty )
set ) ) st
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) is
independent holds
'not' (All ((Ex (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
'<' Ex (
('not' (All (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
A : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ;
theorem
for
Y being ( ( non
empty ) ( non
empty )
set )
for
a being ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Function of
Y : ( ( non
empty ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
for
G being ( ( ) ( )
Subset of ( ( ) ( )
set ) )
for
A,
B being ( ( ) ( non
empty with_non-empty_elements )
a_partition of
Y : ( ( non
empty ) ( non
empty )
set ) ) holds
'not' (Ex ((Ex (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
'<' Ex (
('not' (All (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
A : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ;
theorem
for
Y being ( ( non
empty ) ( non
empty )
set )
for
a being ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Function of
Y : ( ( non
empty ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
for
G being ( ( ) ( )
Subset of ( ( ) ( )
set ) )
for
A,
B being ( ( ) ( non
empty with_non-empty_elements )
a_partition of
Y : ( ( non
empty ) ( non
empty )
set ) ) st
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) is
independent holds
'not' (All ((Ex (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
'<' All (
('not' (All (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
A : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ;
theorem
for
Y being ( ( non
empty ) ( non
empty )
set )
for
a being ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Function of
Y : ( ( non
empty ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
for
G being ( ( ) ( )
Subset of ( ( ) ( )
set ) )
for
A,
B being ( ( ) ( non
empty with_non-empty_elements )
a_partition of
Y : ( ( non
empty ) ( non
empty )
set ) ) st
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) is
independent holds
'not' (Ex ((Ex (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
'<' All (
('not' (All (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
A : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ;
theorem
for
Y being ( ( non
empty ) ( non
empty )
set )
for
a being ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Function of
Y : ( ( non
empty ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
for
G being ( ( ) ( )
Subset of ( ( ) ( )
set ) )
for
A,
B being ( ( ) ( non
empty with_non-empty_elements )
a_partition of
Y : ( ( non
empty ) ( non
empty )
set ) ) holds
'not' (Ex ((Ex (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
'<' Ex (
('not' (Ex (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
A : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ;
theorem
for
Y being ( ( non
empty ) ( non
empty )
set )
for
a being ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Function of
Y : ( ( non
empty ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
for
G being ( ( ) ( )
Subset of ( ( ) ( )
set ) )
for
A,
B being ( ( ) ( non
empty with_non-empty_elements )
a_partition of
Y : ( ( non
empty ) ( non
empty )
set ) ) st
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) is
independent holds
'not' (Ex ((Ex (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
= All (
('not' (Ex (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
A : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ;
theorem
for
Y being ( ( non
empty ) ( non
empty )
set )
for
a being ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Function of
Y : ( ( non
empty ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
for
G being ( ( ) ( )
Subset of ( ( ) ( )
set ) )
for
A,
B being ( ( ) ( non
empty with_non-empty_elements )
a_partition of
Y : ( ( non
empty ) ( non
empty )
set ) ) st
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) is
independent holds
'not' (All ((Ex (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
'<' Ex (
(Ex (('not' a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
A : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ;
theorem
for
Y being ( ( non
empty ) ( non
empty )
set )
for
a being ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Function of
Y : ( ( non
empty ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
for
G being ( ( ) ( )
Subset of ( ( ) ( )
set ) )
for
A,
B being ( ( ) ( non
empty with_non-empty_elements )
a_partition of
Y : ( ( non
empty ) ( non
empty )
set ) ) holds
'not' (Ex ((Ex (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
'<' Ex (
(Ex (('not' a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
A : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ;
theorem
for
Y being ( ( non
empty ) ( non
empty )
set )
for
a being ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Function of
Y : ( ( non
empty ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
for
G being ( ( ) ( )
Subset of ( ( ) ( )
set ) )
for
A,
B being ( ( ) ( non
empty with_non-empty_elements )
a_partition of
Y : ( ( non
empty ) ( non
empty )
set ) ) st
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) is
independent holds
'not' (All ((Ex (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
'<' All (
(Ex (('not' a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
A : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ;
theorem
for
Y being ( ( non
empty ) ( non
empty )
set )
for
a being ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Function of
Y : ( ( non
empty ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
for
G being ( ( ) ( )
Subset of ( ( ) ( )
set ) )
for
A,
B being ( ( ) ( non
empty with_non-empty_elements )
a_partition of
Y : ( ( non
empty ) ( non
empty )
set ) ) st
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) is
independent holds
'not' (Ex ((Ex (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
'<' All (
(Ex (('not' a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
A : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ;
theorem
for
Y being ( ( non
empty ) ( non
empty )
set )
for
a being ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Function of
Y : ( ( non
empty ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
for
G being ( ( ) ( )
Subset of ( ( ) ( )
set ) )
for
A,
B being ( ( ) ( non
empty with_non-empty_elements )
a_partition of
Y : ( ( non
empty ) ( non
empty )
set ) ) holds
'not' (Ex ((Ex (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
'<' Ex (
(All (('not' a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
A : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ;
theorem
for
Y being ( ( non
empty ) ( non
empty )
set )
for
a being ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Function of
Y : ( ( non
empty ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
for
G being ( ( ) ( )
Subset of ( ( ) ( )
set ) )
for
A,
B being ( ( ) ( non
empty with_non-empty_elements )
a_partition of
Y : ( ( non
empty ) ( non
empty )
set ) ) st
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) is
independent holds
'not' (Ex ((Ex (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
= All (
(All (('not' a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
A : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ;
theorem
for
Y being ( ( non
empty ) ( non
empty )
set )
for
a being ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Function of
Y : ( ( non
empty ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
for
G being ( ( ) ( )
Subset of ( ( ) ( )
set ) )
for
A,
B being ( ( ) ( non
empty with_non-empty_elements )
a_partition of
Y : ( ( non
empty ) ( non
empty )
set ) ) st
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) is
independent holds
Ex (
('not' (Ex (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
B : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
'<' 'not' (Ex ((All (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ;
theorem
for
Y being ( ( non
empty ) ( non
empty )
set )
for
a being ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Function of
Y : ( ( non
empty ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
for
G being ( ( ) ( )
Subset of ( ( ) ( )
set ) )
for
A,
B being ( ( ) ( non
empty with_non-empty_elements )
a_partition of
Y : ( ( non
empty ) ( non
empty )
set ) ) holds
All (
('not' (Ex (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
B : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
'<' 'not' (Ex ((All (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ;
theorem
for
Y being ( ( non
empty ) ( non
empty )
set )
for
a being ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Function of
Y : ( ( non
empty ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
for
G being ( ( ) ( )
Subset of ( ( ) ( )
set ) )
for
A,
B being ( ( ) ( non
empty with_non-empty_elements )
a_partition of
Y : ( ( non
empty ) ( non
empty )
set ) ) holds
All (
('not' (Ex (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
B : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
'<' 'not' (All ((Ex (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ;
theorem
for
Y being ( ( non
empty ) ( non
empty )
set )
for
a being ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Function of
Y : ( ( non
empty ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
for
G being ( ( ) ( )
Subset of ( ( ) ( )
set ) )
for
A,
B being ( ( ) ( non
empty with_non-empty_elements )
a_partition of
Y : ( ( non
empty ) ( non
empty )
set ) ) st
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) is
independent holds
All (
('not' (Ex (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
B : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
= 'not' (Ex ((Ex (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ;
theorem
for
Y being ( ( non
empty ) ( non
empty )
set )
for
a being ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Function of
Y : ( ( non
empty ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
for
G being ( ( ) ( )
Subset of ( ( ) ( )
set ) )
for
A,
B being ( ( ) ( non
empty with_non-empty_elements )
a_partition of
Y : ( ( non
empty ) ( non
empty )
set ) ) st
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) is
independent holds
Ex (
('not' (All (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
B : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
= Ex (
('not' (All (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
A : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ;
theorem
for
Y being ( ( non
empty ) ( non
empty )
set )
for
a being ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Function of
Y : ( ( non
empty ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
for
G being ( ( ) ( )
Subset of ( ( ) ( )
set ) )
for
A,
B being ( ( ) ( non
empty with_non-empty_elements )
a_partition of
Y : ( ( non
empty ) ( non
empty )
set ) ) st
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) is
independent holds
All (
('not' (All (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
B : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
'<' Ex (
('not' (All (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
A : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ;
theorem
for
Y being ( ( non
empty ) ( non
empty )
set )
for
a being ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Function of
Y : ( ( non
empty ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
for
G being ( ( ) ( )
Subset of ( ( ) ( )
set ) )
for
A,
B being ( ( ) ( non
empty with_non-empty_elements )
a_partition of
Y : ( ( non
empty ) ( non
empty )
set ) ) st
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) is
independent holds
Ex (
('not' (Ex (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
B : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
'<' Ex (
('not' (All (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
A : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ;
theorem
for
Y being ( ( non
empty ) ( non
empty )
set )
for
a being ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Function of
Y : ( ( non
empty ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
for
G being ( ( ) ( )
Subset of ( ( ) ( )
set ) )
for
A,
B being ( ( ) ( non
empty with_non-empty_elements )
a_partition of
Y : ( ( non
empty ) ( non
empty )
set ) ) holds
All (
('not' (Ex (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
B : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
'<' Ex (
('not' (All (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
A : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ;
theorem
for
Y being ( ( non
empty ) ( non
empty )
set )
for
a being ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Function of
Y : ( ( non
empty ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
for
G being ( ( ) ( )
Subset of ( ( ) ( )
set ) )
for
A,
B being ( ( ) ( non
empty with_non-empty_elements )
a_partition of
Y : ( ( non
empty ) ( non
empty )
set ) ) st
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) is
independent holds
Ex (
('not' (Ex (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
B : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
'<' All (
('not' (All (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
A : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ;
theorem
for
Y being ( ( non
empty ) ( non
empty )
set )
for
a being ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Function of
Y : ( ( non
empty ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
for
G being ( ( ) ( )
Subset of ( ( ) ( )
set ) )
for
A,
B being ( ( ) ( non
empty with_non-empty_elements )
a_partition of
Y : ( ( non
empty ) ( non
empty )
set ) ) st
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) is
independent holds
All (
('not' (Ex (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
B : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
'<' All (
('not' (All (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
A : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ;
theorem
for
Y being ( ( non
empty ) ( non
empty )
set )
for
a being ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Function of
Y : ( ( non
empty ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
for
G being ( ( ) ( )
Subset of ( ( ) ( )
set ) )
for
A,
B being ( ( ) ( non
empty with_non-empty_elements )
a_partition of
Y : ( ( non
empty ) ( non
empty )
set ) ) holds
All (
('not' (Ex (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
B : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
'<' Ex (
('not' (Ex (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
A : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ;
theorem
for
Y being ( ( non
empty ) ( non
empty )
set )
for
a being ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Function of
Y : ( ( non
empty ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
for
G being ( ( ) ( )
Subset of ( ( ) ( )
set ) )
for
A,
B being ( ( ) ( non
empty with_non-empty_elements )
a_partition of
Y : ( ( non
empty ) ( non
empty )
set ) ) st
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) is
independent holds
All (
('not' (Ex (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
B : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
= All (
('not' (Ex (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
A : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ;
theorem
for
Y being ( ( non
empty ) ( non
empty )
set )
for
a being ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Function of
Y : ( ( non
empty ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
for
G being ( ( ) ( )
Subset of ( ( ) ( )
set ) )
for
A,
B being ( ( ) ( non
empty with_non-empty_elements )
a_partition of
Y : ( ( non
empty ) ( non
empty )
set ) ) st
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) is
independent holds
Ex (
('not' (Ex (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
B : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
'<' Ex (
(Ex (('not' a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
A : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ;
theorem
for
Y being ( ( non
empty ) ( non
empty )
set )
for
a being ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Function of
Y : ( ( non
empty ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
for
G being ( ( ) ( )
Subset of ( ( ) ( )
set ) )
for
A,
B being ( ( ) ( non
empty with_non-empty_elements )
a_partition of
Y : ( ( non
empty ) ( non
empty )
set ) ) holds
All (
('not' (Ex (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
B : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
'<' Ex (
(Ex (('not' a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
A : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ;
theorem
for
Y being ( ( non
empty ) ( non
empty )
set )
for
a being ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Function of
Y : ( ( non
empty ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
for
G being ( ( ) ( )
Subset of ( ( ) ( )
set ) )
for
A,
B being ( ( ) ( non
empty with_non-empty_elements )
a_partition of
Y : ( ( non
empty ) ( non
empty )
set ) ) st
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) is
independent holds
Ex (
('not' (Ex (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
B : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
'<' All (
(Ex (('not' a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
A : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ;
theorem
for
Y being ( ( non
empty ) ( non
empty )
set )
for
a being ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Function of
Y : ( ( non
empty ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
for
G being ( ( ) ( )
Subset of ( ( ) ( )
set ) )
for
A,
B being ( ( ) ( non
empty with_non-empty_elements )
a_partition of
Y : ( ( non
empty ) ( non
empty )
set ) ) st
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) is
independent holds
All (
('not' (Ex (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
B : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
'<' All (
(Ex (('not' a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
A : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ;
theorem
for
Y being ( ( non
empty ) ( non
empty )
set )
for
a being ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Function of
Y : ( ( non
empty ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
for
G being ( ( ) ( )
Subset of ( ( ) ( )
set ) )
for
A,
B being ( ( ) ( non
empty with_non-empty_elements )
a_partition of
Y : ( ( non
empty ) ( non
empty )
set ) ) holds
All (
('not' (Ex (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
B : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
'<' Ex (
(All (('not' a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
A : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ;
theorem
for
Y being ( ( non
empty ) ( non
empty )
set )
for
a being ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Function of
Y : ( ( non
empty ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
for
G being ( ( ) ( )
Subset of ( ( ) ( )
set ) )
for
A,
B being ( ( ) ( non
empty with_non-empty_elements )
a_partition of
Y : ( ( non
empty ) ( non
empty )
set ) ) st
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) is
independent holds
All (
('not' (Ex (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
B : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
= All (
(All (('not' a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
A : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ;
theorem
for
Y being ( ( non
empty ) ( non
empty )
set )
for
a being ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Function of
Y : ( ( non
empty ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
for
G being ( ( ) ( )
Subset of ( ( ) ( )
set ) )
for
A,
B being ( ( ) ( non
empty with_non-empty_elements )
a_partition of
Y : ( ( non
empty ) ( non
empty )
set ) ) st
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) is
independent holds
Ex (
(All (('not' a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
B : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
'<' 'not' (Ex ((All (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ;
theorem
for
Y being ( ( non
empty ) ( non
empty )
set )
for
a being ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Function of
Y : ( ( non
empty ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
for
G being ( ( ) ( )
Subset of ( ( ) ( )
set ) )
for
A,
B being ( ( ) ( non
empty with_non-empty_elements )
a_partition of
Y : ( ( non
empty ) ( non
empty )
set ) ) st
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) is
independent holds
All (
(All (('not' a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
B : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
'<' 'not' (Ex ((All (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ;
theorem
for
Y being ( ( non
empty ) ( non
empty )
set )
for
a being ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Function of
Y : ( ( non
empty ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
for
G being ( ( ) ( )
Subset of ( ( ) ( )
set ) )
for
A,
B being ( ( ) ( non
empty with_non-empty_elements )
a_partition of
Y : ( ( non
empty ) ( non
empty )
set ) ) holds
All (
(All (('not' a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
B : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
'<' 'not' (All ((Ex (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ;
theorem
for
Y being ( ( non
empty ) ( non
empty )
set )
for
a being ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Function of
Y : ( ( non
empty ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
for
G being ( ( ) ( )
Subset of ( ( ) ( )
set ) )
for
A,
B being ( ( ) ( non
empty with_non-empty_elements )
a_partition of
Y : ( ( non
empty ) ( non
empty )
set ) ) st
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) is
independent holds
All (
(All (('not' a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
B : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
'<' 'not' (Ex ((Ex (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ;
theorem
for
Y being ( ( non
empty ) ( non
empty )
set )
for
a being ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Function of
Y : ( ( non
empty ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
for
G being ( ( ) ( )
Subset of ( ( ) ( )
set ) )
for
A,
B being ( ( ) ( non
empty with_non-empty_elements )
a_partition of
Y : ( ( non
empty ) ( non
empty )
set ) ) st
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) is
independent holds
Ex (
(Ex (('not' a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
B : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
'<' Ex (
('not' (All (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
A : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ;
theorem
for
Y being ( ( non
empty ) ( non
empty )
set )
for
a being ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Function of
Y : ( ( non
empty ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
for
G being ( ( ) ( )
Subset of ( ( ) ( )
set ) )
for
A,
B being ( ( ) ( non
empty with_non-empty_elements )
a_partition of
Y : ( ( non
empty ) ( non
empty )
set ) ) st
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) is
independent holds
All (
(Ex (('not' a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
B : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
'<' Ex (
('not' (All (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
A : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ;
theorem
for
Y being ( ( non
empty ) ( non
empty )
set )
for
a being ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Function of
Y : ( ( non
empty ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
for
G being ( ( ) ( )
Subset of ( ( ) ( )
set ) )
for
A,
B being ( ( ) ( non
empty with_non-empty_elements )
a_partition of
Y : ( ( non
empty ) ( non
empty )
set ) ) st
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) is
independent holds
Ex (
(All (('not' a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
B : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
'<' Ex (
('not' (All (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
A : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ;
theorem
for
Y being ( ( non
empty ) ( non
empty )
set )
for
a being ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Function of
Y : ( ( non
empty ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
for
G being ( ( ) ( )
Subset of ( ( ) ( )
set ) )
for
A,
B being ( ( ) ( non
empty with_non-empty_elements )
a_partition of
Y : ( ( non
empty ) ( non
empty )
set ) ) holds
All (
(All (('not' a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
B : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
'<' Ex (
('not' (All (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
A : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ;
theorem
for
Y being ( ( non
empty ) ( non
empty )
set )
for
a being ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Function of
Y : ( ( non
empty ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
for
G being ( ( ) ( )
Subset of ( ( ) ( )
set ) )
for
A,
B being ( ( ) ( non
empty with_non-empty_elements )
a_partition of
Y : ( ( non
empty ) ( non
empty )
set ) ) st
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) is
independent holds
Ex (
(All (('not' a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
B : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
'<' All (
('not' (All (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
A : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ;
theorem
for
Y being ( ( non
empty ) ( non
empty )
set )
for
a being ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Function of
Y : ( ( non
empty ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
for
G being ( ( ) ( )
Subset of ( ( ) ( )
set ) )
for
A,
B being ( ( ) ( non
empty with_non-empty_elements )
a_partition of
Y : ( ( non
empty ) ( non
empty )
set ) ) st
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) is
independent holds
All (
(All (('not' a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
B : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
'<' All (
('not' (All (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
A : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ;
theorem
for
Y being ( ( non
empty ) ( non
empty )
set )
for
a being ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Function of
Y : ( ( non
empty ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
for
G being ( ( ) ( )
Subset of ( ( ) ( )
set ) )
for
A,
B being ( ( ) ( non
empty with_non-empty_elements )
a_partition of
Y : ( ( non
empty ) ( non
empty )
set ) ) holds
All (
(All (('not' a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
B : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
'<' Ex (
('not' (Ex (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
A : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ;
theorem
for
Y being ( ( non
empty ) ( non
empty )
set )
for
a being ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Function of
Y : ( ( non
empty ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
for
G being ( ( ) ( )
Subset of ( ( ) ( )
set ) )
for
A,
B being ( ( ) ( non
empty with_non-empty_elements )
a_partition of
Y : ( ( non
empty ) ( non
empty )
set ) ) st
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) is
independent holds
All (
(All (('not' a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
B : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
= All (
('not' (Ex (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
A : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ;
theorem
for
Y being ( ( non
empty ) ( non
empty )
set )
for
a being ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Function of
Y : ( ( non
empty ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
for
G being ( ( ) ( )
Subset of ( ( ) ( )
set ) )
for
A,
B being ( ( ) ( non
empty with_non-empty_elements )
a_partition of
Y : ( ( non
empty ) ( non
empty )
set ) ) holds
All (
(Ex (('not' a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
B : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
'<' Ex (
(Ex (('not' a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
A : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ;
theorem
for
Y being ( ( non
empty ) ( non
empty )
set )
for
a being ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Function of
Y : ( ( non
empty ) ( non
empty )
set ) ,
BOOLEAN : ( ( ) ( non
empty )
set ) )
for
G being ( ( ) ( )
Subset of ( ( ) ( )
set ) )
for
A,
B being ( ( ) ( non
empty with_non-empty_elements )
a_partition of
Y : ( ( non
empty ) ( non
empty )
set ) ) st
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) is
independent holds
Ex (
(All (('not' a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,A : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
B : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) )
'<' Ex (
(Ex (('not' a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,B : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ,
A : ( ( ) ( non
empty with_non-empty_elements )
a_partition of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
G : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like quasi_total ) (
Function-like quasi_total boolean-valued )
Element of
bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ;