:: PARTIT_2 semantic presentation

begin

definition
let Y be ( ( non empty ) ( non empty ) set ) ;
let G be ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty ) set ) ) ;
:: original: Element
redefine mode Element of G -> ( ( ) ( non empty with_non-empty_elements ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) ;
end;

theorem :: PARTIT_2:1
for Y being ( ( non empty ) ( non empty ) set ) holds '/\' ({} (PARTITIONS Y : ( ( non empty ) ( non empty ) set ) ) : ( ( partition-membered ) ( non empty partition-membered ) Element of bool (bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( empty proper Relation-like non-empty empty-yielding Function-like one-to-one constant functional V56() ) Element of bool (PARTITIONS b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( partition-membered ) ( non empty partition-membered ) Element of bool (bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) = %O Y : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ;

theorem :: PARTIT_2:2
for Y being ( ( non empty ) ( non empty ) set )
for R, S being ( ( V17(b1 : ( ( non empty ) ( non empty ) set ) ) symmetric transitive ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued V17(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total reflexive symmetric transitive ) Equivalence_Relation of ) holds R : ( ( V17(b1 : ( ( non empty ) ( non empty ) set ) ) symmetric transitive ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued V17(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total reflexive symmetric transitive ) Equivalence_Relation of ) \/ S : ( ( V17(b1 : ( ( non empty ) ( non empty ) set ) ) symmetric transitive ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued V17(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total reflexive symmetric transitive ) Equivalence_Relation of ) : ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued ) Element of bool ([#] (b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) )) : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) c= R : ( ( V17(b1 : ( ( non empty ) ( non empty ) set ) ) symmetric transitive ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued V17(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total reflexive symmetric transitive ) Equivalence_Relation of ) * S : ( ( V17(b1 : ( ( non empty ) ( non empty ) set ) ) symmetric transitive ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued V17(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total reflexive symmetric transitive ) Equivalence_Relation of ) : ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued ) Element of bool ([#] (b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) )) : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: PARTIT_2:3
for Y being ( ( non empty ) ( non empty ) set )
for R being ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued ) Relation of ) holds R : ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued ) Relation of ) c= nabla Y : ( ( non empty ) ( non empty ) set ) : ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued V17(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total reflexive symmetric transitive ) Element of bool ([#] (b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) )) : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: PARTIT_2:4
for Y being ( ( non empty ) ( non empty ) set )
for R being ( ( V17(b1 : ( ( non empty ) ( non empty ) set ) ) symmetric transitive ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued V17(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total reflexive symmetric transitive ) Equivalence_Relation of ) holds
( (nabla Y : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued V17(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total reflexive symmetric transitive ) Element of bool ([#] (b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) )) : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) * R : ( ( V17(b1 : ( ( non empty ) ( non empty ) set ) ) symmetric transitive ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued V17(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total reflexive symmetric transitive ) Equivalence_Relation of ) : ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued ) Element of bool ([#] (b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) )) : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) = nabla Y : ( ( non empty ) ( non empty ) set ) : ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued V17(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total reflexive symmetric transitive ) Element of bool ([#] (b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) )) : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) & R : ( ( V17(b1 : ( ( non empty ) ( non empty ) set ) ) symmetric transitive ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued V17(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total reflexive symmetric transitive ) Equivalence_Relation of ) * (nabla Y : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued V17(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total reflexive symmetric transitive ) Element of bool ([#] (b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) )) : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued ) Element of bool ([#] (b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) )) : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) = nabla Y : ( ( non empty ) ( non empty ) set ) : ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued V17(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total reflexive symmetric transitive ) Element of bool ([#] (b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) )) : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: PARTIT_2:5
for Y being ( ( non empty ) ( non empty ) set )
for P being ( ( ) ( non empty with_non-empty_elements ) a_partition of Y : ( ( non empty ) ( non empty ) set ) )
for x, y being ( ( ) ( ) Element of Y : ( ( non empty ) ( non empty ) set ) ) holds
( [x : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ] : ( ( ) ( ) set ) in ERl P : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( V17(b1 : ( ( non empty ) ( non empty ) set ) ) symmetric transitive ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued V17(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total reflexive symmetric transitive ) Element of bool ([#] (b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) )) : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) iff x : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) in EqClass (y : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ,P : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of b2 : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ) ) ;

theorem :: PARTIT_2:6
for Y being ( ( non empty ) ( non empty ) set )
for P, Q, R being ( ( ) ( non empty with_non-empty_elements ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) st ERl R : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( V17(b1 : ( ( non empty ) ( non empty ) set ) ) symmetric transitive ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued V17(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total reflexive symmetric transitive ) Element of bool ([#] (b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) )) : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) = (ERl P : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( V17(b1 : ( ( non empty ) ( non empty ) set ) ) symmetric transitive ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued V17(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total reflexive symmetric transitive ) Element of bool ([#] (b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) )) : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) * (ERl Q : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( V17(b1 : ( ( non empty ) ( non empty ) set ) ) symmetric transitive ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued V17(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total reflexive symmetric transitive ) Element of bool ([#] (b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) )) : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued ) Element of bool ([#] (b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) )) : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) holds
for x, y being ( ( ) ( ) Element of Y : ( ( non empty ) ( non empty ) set ) ) holds
( x : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) in EqClass (y : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ,R : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of b4 : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ) iff ex z being ( ( ) ( ) Element of Y : ( ( non empty ) ( non empty ) set ) ) st
( x : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) in EqClass (z : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ,P : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of b2 : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ) & z : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) in EqClass (y : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ,Q : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of b3 : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ) ) ) ;

theorem :: PARTIT_2:7
for R, S being ( ( Relation-like ) ( Relation-like ) Relation)
for Y being ( ( ) ( ) set ) st R : ( ( Relation-like ) ( Relation-like ) Relation) is_reflexive_in Y : ( ( ) ( ) set ) & S : ( ( Relation-like ) ( Relation-like ) Relation) is_reflexive_in Y : ( ( ) ( ) set ) holds
R : ( ( Relation-like ) ( Relation-like ) Relation) * S : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( Relation-like ) ( Relation-like ) set ) is_reflexive_in Y : ( ( ) ( ) set ) ;

theorem :: PARTIT_2:8
for R being ( ( Relation-like ) ( Relation-like ) Relation)
for Y being ( ( ) ( ) set ) st R : ( ( Relation-like ) ( Relation-like ) Relation) is_reflexive_in Y : ( ( ) ( ) set ) holds
Y : ( ( ) ( ) set ) c= field R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) ;

theorem :: PARTIT_2:9
for Y being ( ( ) ( ) set )
for R being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Relation of ) st R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Relation of ) is_reflexive_in Y : ( ( ) ( ) set ) holds
Y : ( ( ) ( ) set ) = field R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Relation of ) : ( ( ) ( ) set ) ;

theorem :: PARTIT_2:10
for Y being ( ( non empty ) ( non empty ) set )
for R, S being ( ( V17(b1 : ( ( non empty ) ( non empty ) set ) ) symmetric transitive ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued V17(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total reflexive symmetric transitive ) Equivalence_Relation of ) st R : ( ( V17(b1 : ( ( non empty ) ( non empty ) set ) ) symmetric transitive ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued V17(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total reflexive symmetric transitive ) Equivalence_Relation of ) * S : ( ( V17(b1 : ( ( non empty ) ( non empty ) set ) ) symmetric transitive ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued V17(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total reflexive symmetric transitive ) Equivalence_Relation of ) : ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued ) Element of bool ([#] (b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) )) : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) = S : ( ( V17(b1 : ( ( non empty ) ( non empty ) set ) ) symmetric transitive ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued V17(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total reflexive symmetric transitive ) Equivalence_Relation of ) * R : ( ( V17(b1 : ( ( non empty ) ( non empty ) set ) ) symmetric transitive ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued V17(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total reflexive symmetric transitive ) Equivalence_Relation of ) : ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued ) Element of bool ([#] (b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) )) : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) holds
R : ( ( V17(b1 : ( ( non empty ) ( non empty ) set ) ) symmetric transitive ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued V17(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total reflexive symmetric transitive ) Equivalence_Relation of ) * S : ( ( V17(b1 : ( ( non empty ) ( non empty ) set ) ) symmetric transitive ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued V17(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total reflexive symmetric transitive ) Equivalence_Relation of ) : ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued ) Element of bool ([#] (b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) )) : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) is ( ( V17(b1 : ( ( non empty ) ( non empty ) set ) ) symmetric transitive ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued V17(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total reflexive symmetric transitive ) Equivalence_Relation of ) ;

begin

theorem :: PARTIT_2:11
for Y being ( ( non empty ) ( non empty ) set )
for a, b being ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like V17(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) st a : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like V17(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '<' b : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like V17(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds
'not' b : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like V17(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like V17(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total boolean-valued ) Element of bool ([#] (b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) '<' 'not' a : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like V17(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like V17(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total boolean-valued ) Element of bool ([#] (b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: PARTIT_2:12
for Y being ( ( non empty ) ( non empty ) set )
for a, b being ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like V17(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for G being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for P being ( ( ) ( non empty with_non-empty_elements ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) st a : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like V17(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '<' b : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like V17(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds
All (a : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like V17(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,P : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like V17(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total boolean-valued ) Element of bool ([#] (b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) '<' All (b : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like V17(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,P : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like V17(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total boolean-valued ) Element of bool ([#] (b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: PARTIT_2:13
for Y being ( ( non empty ) ( non empty ) set )
for a, b being ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like V17(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for G being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for P being ( ( ) ( non empty with_non-empty_elements ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) st a : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like V17(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '<' b : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like V17(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds
Ex (a : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like V17(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,P : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like V17(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total boolean-valued ) Element of bool ([#] (b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) '<' Ex (b : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like V17(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,P : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like V17(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total boolean-valued ) Element of bool ([#] (b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ;

begin

theorem :: PARTIT_2:14
for Y being ( ( non empty ) ( non empty ) set )
for G being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) st G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) is independent holds
for P, Q being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) st P : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) c= G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) & Q : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) c= G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds
(ERl ('/\' P : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( V17(b1 : ( ( non empty ) ( non empty ) set ) ) symmetric transitive ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued V17(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total reflexive symmetric transitive ) Element of bool ([#] (b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) )) : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) * (ERl ('/\' Q : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( V17(b1 : ( ( non empty ) ( non empty ) set ) ) symmetric transitive ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued V17(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total reflexive symmetric transitive ) Element of bool ([#] (b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) )) : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued ) Element of bool ([#] (b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) )) : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) = (ERl ('/\' Q : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( V17(b1 : ( ( non empty ) ( non empty ) set ) ) symmetric transitive ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued V17(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total reflexive symmetric transitive ) Element of bool ([#] (b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) )) : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) * (ERl ('/\' P : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( V17(b1 : ( ( non empty ) ( non empty ) set ) ) symmetric transitive ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued V17(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total reflexive symmetric transitive ) Element of bool ([#] (b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) )) : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued ) Element of bool ([#] (b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) )) : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: PARTIT_2:15
for Y being ( ( non empty ) ( non empty ) set )
for a being ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like V17(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for G being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for P, Q being ( ( ) ( non empty with_non-empty_elements ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) st G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) is independent holds
All ((All (a : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like V17(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,P : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) )) : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like V17(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total boolean-valued ) Element of bool ([#] (b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ,Q : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like V17(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total boolean-valued ) Element of bool ([#] (b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) = All ((All (a : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like V17(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,Q : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) )) : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like V17(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total boolean-valued ) Element of bool ([#] (b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ,P : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like V17(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total boolean-valued ) Element of bool ([#] (b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: PARTIT_2:16
for Y being ( ( non empty ) ( non empty ) set )
for a being ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like V17(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for G being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for P, Q being ( ( ) ( non empty with_non-empty_elements ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) st G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) is independent holds
Ex ((Ex (a : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like V17(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,P : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) )) : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like V17(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total boolean-valued ) Element of bool ([#] (b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ,Q : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like V17(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total boolean-valued ) Element of bool ([#] (b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) = Ex ((Ex (a : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like V17(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,Q : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) )) : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like V17(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total boolean-valued ) Element of bool ([#] (b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ,P : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like V17(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total boolean-valued ) Element of bool ([#] (b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: PARTIT_2:17
for Y being ( ( non empty ) ( non empty ) set )
for a being ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like V17(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for G being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for P, Q being ( ( ) ( non empty with_non-empty_elements ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) st G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) is independent holds
Ex ((All (a : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like V17(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,P : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) )) : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like V17(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total boolean-valued ) Element of bool ([#] (b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ,Q : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like V17(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total boolean-valued ) Element of bool ([#] (b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) '<' All ((Ex (a : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like V17(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,Q : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) )) : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like V17(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total boolean-valued ) Element of bool ([#] (b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ,P : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like V17(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total boolean-valued ) Element of bool ([#] (b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ;

begin

notation
let A, B be ( ( ) ( ) set ) ;
synonym [#] (A,B) for [:A,B:];
end;

definition
let A, B be ( ( ) ( ) set ) ;
func {} (A,B) -> ( ( ) ( Relation-like A : ( ( non empty ) ( non empty ) set ) -defined B : ( ( Function-like quasi_total ) ( non empty Relation-like A : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like V17(A : ( ( non empty ) ( non empty ) set ) ) quasi_total boolean-valued ) Element of bool ([#] (A : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) -valued ) Relation of ,) equals :: PARTIT_2:def 1
 {} : ( ( ) ( empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional V56() ) set ) ;
:: original: [#]
redefine func [#] (A,B) -> ( ( ) ( Relation-like A : ( ( non empty ) ( non empty ) set ) -defined B : ( ( Function-like quasi_total ) ( non empty Relation-like A : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like V17(A : ( ( non empty ) ( non empty ) set ) ) quasi_total boolean-valued ) Element of bool ([#] (A : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) -valued ) Relation of ,) ;
end;

registration
let A, B be ( ( ) ( ) set ) ;
cluster {} (A : ( ( ) ( ) set ) ,B : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like A : ( ( ) ( ) set ) -defined B : ( ( ) ( ) set ) -valued ) Relation of ,) -> empty ;
end;

theorem :: PARTIT_2:18
for X being ( ( non empty ) ( non empty ) set ) holds field (id X : ( ( non empty ) ( non empty ) set ) ) : ( ( Relation-like ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like one-to-one V17(b1 : ( ( non empty ) ( non empty ) set ) ) reflexive symmetric antisymmetric transitive ) set ) : ( ( ) ( ) set ) = X : ( ( non empty ) ( non empty ) set ) ;

theorem :: PARTIT_2:19
op1 : ( ( Function-like quasi_total ) ( non empty Relation-like 1 : ( ( ) ( non empty ) set ) -defined 1 : ( ( ) ( non empty ) set ) -valued Function-like V17(1 : ( ( ) ( non empty ) set ) ) quasi_total ) Element of bool ([#] (1 : ( ( ) ( non empty ) set ) ,1 : ( ( ) ( non empty ) set ) )) : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) = {[{} : ( ( ) ( empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional V56() ) set ) ,{} : ( ( ) ( empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional V56() ) set ) ] : ( ( ) ( ) set ) } : ( ( ) ( non empty Relation-like Function-like ) set ) ;

theorem :: PARTIT_2:20
for A, B being ( ( ) ( ) set ) holds field ({} (A : ( ( ) ( ) set ) ,B : ( ( ) ( ) set ) )) : ( ( ) ( empty Relation-like non-empty empty-yielding b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued Function-like one-to-one constant functional V56() ) Relation of ,) : ( ( ) ( ) set ) = {} : ( ( ) ( empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional V56() ) set ) ;

theorem :: PARTIT_2:21
for X being ( ( non empty ) ( non empty ) set )
for R being ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued ) Relation of ) st R : ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued ) Relation of ) is_reflexive_in X : ( ( non empty ) ( non empty ) set ) holds
( R : ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued ) Relation of ) is reflexive & field R : ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued ) Relation of ) : ( ( ) ( ) set ) = X : ( ( non empty ) ( non empty ) set ) ) ;

theorem :: PARTIT_2:22
for X being ( ( non empty ) ( non empty ) set )
for R being ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued ) Relation of ) st R : ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued ) Relation of ) is_symmetric_in X : ( ( non empty ) ( non empty ) set ) holds
R : ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued ) Relation of ) is symmetric ;

theorem :: PARTIT_2:23
for X, S being ( ( non empty ) ( non empty ) set )
for R being ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued ) Relation of ) st R : ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued ) Relation of ) is symmetric holds
R : ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued ) Relation of ) is_symmetric_in S : ( ( non empty ) ( non empty ) set ) ;

theorem :: PARTIT_2:24
for X, S being ( ( non empty ) ( non empty ) set )
for R being ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued ) Relation of ) st R : ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued ) Relation of ) is antisymmetric holds
R : ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued ) Relation of ) is_antisymmetric_in S : ( ( non empty ) ( non empty ) set ) ;

theorem :: PARTIT_2:25
for X being ( ( non empty ) ( non empty ) set )
for R being ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued ) Relation of ) st R : ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued ) Relation of ) is_antisymmetric_in X : ( ( non empty ) ( non empty ) set ) holds
R : ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued ) Relation of ) is antisymmetric ;

theorem :: PARTIT_2:26
for X, S being ( ( non empty ) ( non empty ) set )
for R being ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued ) Relation of ) st R : ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued ) Relation of ) is transitive holds
R : ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued ) Relation of ) is_transitive_in S : ( ( non empty ) ( non empty ) set ) ;

theorem :: PARTIT_2:27
for X being ( ( non empty ) ( non empty ) set )
for R being ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued ) Relation of ) st R : ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued ) Relation of ) is_transitive_in X : ( ( non empty ) ( non empty ) set ) holds
R : ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued ) Relation of ) is transitive ;

theorem :: PARTIT_2:28
for X, S being ( ( non empty ) ( non empty ) set )
for R being ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued ) Relation of ) st R : ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued ) Relation of ) is asymmetric holds
R : ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued ) Relation of ) is_asymmetric_in S : ( ( non empty ) ( non empty ) set ) ;

theorem :: PARTIT_2:29
for X being ( ( non empty ) ( non empty ) set )
for R being ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued ) Relation of ) st R : ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued ) Relation of ) is_asymmetric_in X : ( ( non empty ) ( non empty ) set ) holds
R : ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued ) Relation of ) is asymmetric ;

theorem :: PARTIT_2:30
for X, S being ( ( non empty ) ( non empty ) set )
for R being ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued ) Relation of ) st R : ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued ) Relation of ) is irreflexive & field R : ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued ) Relation of ) : ( ( ) ( ) set ) c= S : ( ( non empty ) ( non empty ) set ) holds
R : ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued ) Relation of ) is_irreflexive_in S : ( ( non empty ) ( non empty ) set ) ;

theorem :: PARTIT_2:31
for X being ( ( non empty ) ( non empty ) set )
for R being ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued ) Relation of ) st R : ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued ) Relation of ) is_irreflexive_in X : ( ( non empty ) ( non empty ) set ) holds
R : ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued ) Relation of ) is irreflexive ;

registration
cluster empty Relation-like -> Relation-like irreflexive asymmetric transitive for ( ( ) ( ) set ) ;
end;

definition
let f be ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ;
attr f is involutive means :: PARTIT_2:def 2
 for x being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) in dom f : ( ( ) ( ) set ) : ( ( ) ( ) set ) holds
f : ( ( ) ( ) set ) . (f : ( ( ) ( ) set ) . x : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) = x : ( ( ) ( ) set ) ;
end;

definition
let X be ( ( non empty ) ( non empty ) set ) ;
let f be ( ( Function-like quasi_total ) ( non empty Relation-like X : ( ( non empty ) ( non empty ) set ) -defined X : ( ( non empty ) ( non empty ) set ) -valued Function-like V17(X : ( ( non empty ) ( non empty ) set ) ) quasi_total ) UnOp of X : ( ( non empty ) ( non empty ) set ) ) ;
:: original: involutive
redefine attr f is involutive means :: PARTIT_2:def 3
 for x being ( ( ) ( ) Element of X : ( ( ) ( ) set ) ) holds f : ( ( ) ( ) set ) . (f : ( ( ) ( ) set ) . x : ( ( ) ( ) Element of X : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of X : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of X : ( ( ) ( ) set ) ) = x : ( ( ) ( ) Element of X : ( ( non empty ) ( non empty ) set ) ) ;
end;

registration
cluster op1 : ( ( ) ( ) set ) -> Relation-like Function-like involutive for ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ;
end;

registration
let X be ( ( ) ( ) set ) ;
cluster id X : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like X : ( ( ) ( ) set ) -defined X : ( ( ) ( ) set ) -valued Function-like one-to-one V17(X : ( ( ) ( ) set ) ) reflexive symmetric antisymmetric transitive ) set ) -> Relation-like involutive ;
end;