:: RELSET_2 semantic presentation

begin

notation
let X be ( ( ) ( ) set ) ;
synonym {_{X}_} for SmallestPartition X;
end;

theorem :: RELSET_2:1
for y, X being ( ( ) ( ) set ) holds
( y : ( ( ) ( ) set ) in {_{X : ( ( ) ( ) set ) }_} : ( ( ) ( ) a_partition of b2 : ( ( ) ( ) set ) ) iff ex x being ( ( ) ( ) set ) st
( y : ( ( ) ( ) set ) = {x : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) & x : ( ( ) ( ) set ) in X : ( ( ) ( ) set ) ) ) ;

theorem :: RELSET_2:2
for X being ( ( ) ( ) set ) holds
( X : ( ( ) ( ) set ) = {} : ( ( ) ( empty Relation-like non-empty empty-yielding ) set ) iff {_{X : ( ( ) ( ) set ) }_} : ( ( ) ( ) a_partition of b1 : ( ( ) ( ) set ) ) = {} : ( ( ) ( empty Relation-like non-empty empty-yielding ) set ) ) ;

theorem :: RELSET_2:3
for X, Y being ( ( ) ( ) set ) holds {_{(X : ( ( ) ( ) set ) \/ Y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) }_} : ( ( ) ( ) a_partition of b1 : ( ( ) ( ) set ) \/ b2 : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) = {_{X : ( ( ) ( ) set ) }_} : ( ( ) ( ) a_partition of b1 : ( ( ) ( ) set ) ) \/ {_{Y : ( ( ) ( ) set ) }_} : ( ( ) ( ) a_partition of b2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ;

theorem :: RELSET_2:4
for X, Y being ( ( ) ( ) set ) holds {_{(X : ( ( ) ( ) set ) /\ Y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) }_} : ( ( ) ( ) a_partition of b1 : ( ( ) ( ) set ) /\ b2 : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) = {_{X : ( ( ) ( ) set ) }_} : ( ( ) ( ) a_partition of b1 : ( ( ) ( ) set ) ) /\ {_{Y : ( ( ) ( ) set ) }_} : ( ( ) ( ) a_partition of b2 : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of bool (bool b2 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: RELSET_2:5
for X, Y being ( ( ) ( ) set ) holds {_{(X : ( ( ) ( ) set ) \ Y : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) }_} : ( ( ) ( ) a_partition of b1 : ( ( ) ( ) set ) \ b2 : ( ( ) ( ) set ) : ( ( ) ( ) Element of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) = {_{X : ( ( ) ( ) set ) }_} : ( ( ) ( ) a_partition of b1 : ( ( ) ( ) set ) ) \ {_{Y : ( ( ) ( ) set ) }_} : ( ( ) ( ) a_partition of b2 : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: RELSET_2:6
for X, Y being ( ( ) ( ) set ) holds
( X : ( ( ) ( ) set ) c= Y : ( ( ) ( ) set ) iff {_{X : ( ( ) ( ) set ) }_} : ( ( ) ( ) a_partition of b1 : ( ( ) ( ) set ) ) c= {_{Y : ( ( ) ( ) set ) }_} : ( ( ) ( ) a_partition of b2 : ( ( ) ( ) set ) ) ) ;

theorem :: RELSET_2:7
for M being ( ( ) ( ) set )
for B1, B2 being ( ( ) ( ) Subset-Family of ) holds (Intersect B1 : ( ( ) ( ) Subset-Family of ) ) : ( ( ) ( ) Element of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) /\ (Intersect B2 : ( ( ) ( ) Subset-Family of ) ) : ( ( ) ( ) Element of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) c= Intersect (B1 : ( ( ) ( ) Subset-Family of ) /\ B2 : ( ( ) ( ) Subset-Family of ) ) : ( ( ) ( ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: RELSET_2:8
errorfrm ;

begin

theorem :: RELSET_2:9
for y, x being ( ( ) ( ) set )
for R being ( ( Relation-like ) ( Relation-like ) Relation) holds
( y : ( ( ) ( ) set ) in Im (R : ( ( Relation-like ) ( Relation-like ) Relation) ,x : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) iff [x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) ] : ( ( ) ( V18() ) set ) in R : ( ( Relation-like ) ( Relation-like ) Relation) ) ;

theorem :: RELSET_2:10
for x being ( ( ) ( ) set )
for R1, R2 being ( ( Relation-like ) ( Relation-like ) Relation) holds Im ((R1 : ( ( Relation-like ) ( Relation-like ) Relation) \/ R2 : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( Relation-like ) set ) ,x : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) = (Im (R1 : ( ( Relation-like ) ( Relation-like ) Relation) ,x : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) \/ (Im (R2 : ( ( Relation-like ) ( Relation-like ) Relation) ,x : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

theorem :: RELSET_2:11
for x being ( ( ) ( ) set )
for R1, R2 being ( ( Relation-like ) ( Relation-like ) Relation) holds Im ((R1 : ( ( Relation-like ) ( Relation-like ) Relation) /\ R2 : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( Relation-like ) set ) ,x : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) = (Im (R1 : ( ( Relation-like ) ( Relation-like ) Relation) ,x : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) /\ (Im (R2 : ( ( Relation-like ) ( Relation-like ) Relation) ,x : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

theorem :: RELSET_2:12
for x being ( ( ) ( ) set )
for R1, R2 being ( ( Relation-like ) ( Relation-like ) Relation) holds Im ((R1 : ( ( Relation-like ) ( Relation-like ) Relation) \ R2 : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( Relation-like ) Element of bool b2 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( non empty ) set ) ) ,x : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) = (Im (R1 : ( ( Relation-like ) ( Relation-like ) Relation) ,x : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) \ (Im (R2 : ( ( Relation-like ) ( Relation-like ) Relation) ,x : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) : ( ( ) ( ) Element of bool (Im (b2 : ( ( Relation-like ) ( Relation-like ) Relation) ,b1 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: RELSET_2:13
for X being ( ( ) ( ) set )
for R1, R2 being ( ( Relation-like ) ( Relation-like ) Relation) holds (R1 : ( ( Relation-like ) ( Relation-like ) Relation) /\ R2 : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( Relation-like ) set ) .: {_{X : ( ( ) ( ) set ) }_} : ( ( ) ( ) a_partition of b1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) c= (R1 : ( ( Relation-like ) ( Relation-like ) Relation) .: {_{X : ( ( ) ( ) set ) }_} : ( ( ) ( ) a_partition of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) /\ (R2 : ( ( Relation-like ) ( Relation-like ) Relation) .: {_{X : ( ( ) ( ) set ) }_} : ( ( ) ( ) a_partition of b1 : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

definition
let X, Y be ( ( ) ( ) set ) ;
let R be ( ( ) ( Relation-like X : ( ( ) ( ) set ) -defined Y : ( ( ) ( ) set ) -valued ) Relation of ,) ;
let x be ( ( ) ( ) set ) ;
:: original: Im
redefine func Im (R,x) -> ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;
:: original: Coim
redefine func Coim (R,x) -> ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;
end;

theorem :: RELSET_2:14
for A being ( ( ) ( ) set )
for F being ( ( ) ( ) Subset-Family of )
for R being ( ( Relation-like ) ( Relation-like ) Relation) holds R : ( ( Relation-like ) ( Relation-like ) Relation) .: (union F : ( ( ) ( ) Subset-Family of ) ) : ( ( ) ( ) Element of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) = union { (R : ( ( Relation-like ) ( Relation-like ) Relation) .: X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) where X is ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) in F : ( ( ) ( ) Subset-Family of ) } : ( ( ) ( ) set ) ;

theorem :: RELSET_2:15
for A being ( ( non empty ) ( non empty ) set )
for X being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) = union { {x : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) } : ( ( ) ( non empty ) set ) where x is ( ( ) ( ) Element of A : ( ( non empty ) ( non empty ) set ) ) : x : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) in X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) } : ( ( ) ( ) set ) ;

theorem :: RELSET_2:16
for A being ( ( non empty ) ( non empty ) set )
for X being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds { {x : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) } : ( ( ) ( non empty ) set ) where x is ( ( ) ( ) Element of A : ( ( non empty ) ( non empty ) set ) ) : x : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) in X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) } is ( ( ) ( ) Subset-Family of ) ;

theorem :: RELSET_2:17
for A being ( ( non empty ) ( non empty ) set )
for B being ( ( ) ( ) set )
for X being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for R being ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Relation of ,) holds R : ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Relation of ,) .: X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool b2 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = union { (Class (R : ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Relation of ,) ,x : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) )) : ( ( ) ( ) Element of bool b2 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) where x is ( ( ) ( ) Element of A : ( ( non empty ) ( non empty ) set ) ) : x : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) in X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) } : ( ( ) ( ) set ) ;

theorem :: RELSET_2:18
for A being ( ( non empty ) ( non empty ) set )
for B being ( ( ) ( ) set )
for X being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for R being ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Relation of ,) holds { (R : ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Relation of ,) .: x : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool b2 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) where x is ( ( ) ( ) Element of A : ( ( non empty ) ( non empty ) set ) ) : x : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) in X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) } is ( ( ) ( ) Subset-Family of ) ;

definition
let A be ( ( ) ( ) set ) ;
let R be ( ( Relation-like ) ( Relation-like ) Relation) ;
func .: (R,A) -> ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) means :: RELSET_2:def 1
( dom it : ( ( ) ( ) a_partition of A : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) = bool A : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool A : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) & ( for X being ( ( ) ( ) set ) st X : ( ( ) ( ) set ) c= A : ( ( non empty ) ( non empty ) set ) holds
it : ( ( ) ( ) a_partition of A : ( ( non empty ) ( non empty ) set ) ) . X : ( ( ) ( ) set ) : ( ( ) ( ) set ) = R : ( ( non empty partition-membered ) ( non empty partition-membered ) Element of bool (bool (bool A : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool A : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) .: X : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) );
end;

notation
let B, A be ( ( ) ( ) set ) ;
let R be ( ( ) ( Relation-like A : ( ( ) ( ) set ) -defined B : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) ;
synonym .: R for .: (A,B);
end;

theorem :: RELSET_2:19
for X, A, B being ( ( ) ( ) set )
for R being ( ( ) ( Relation-like b2 : ( ( ) ( ) set ) -defined b3 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) st X : ( ( ) ( ) set ) in dom (.: ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) holds
(.: ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) . X : ( ( ) ( ) set ) : ( ( ) ( ) set ) = R : ( ( ) ( Relation-like b2 : ( ( ) ( ) set ) -defined b3 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) .: X : ( ( ) ( ) set ) : ( ( ) ( ) Element of bool b3 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: RELSET_2:20
for A, B being ( ( ) ( ) set )
for R being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) holds rng (.: ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) c= bool (rng R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool b2 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool (rng b3 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool b2 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: RELSET_2:21
for A, B being ( ( ) ( ) set )
for R being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) holds .: : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) is ( ( Function-like V21( bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) , bool (rng b3 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool b2 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool (rng b3 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool b2 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -defined bool (rng b3 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool b2 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool (rng b3 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool b2 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V21( bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) , bool (rng b3 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool b2 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool (rng b3 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool b2 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) Function of bool A : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) , bool (rng R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool b2 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool (rng b3 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool b2 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ;

definition
let B, A be ( ( ) ( ) set ) ;
let R be ( ( ) ( Relation-like A : ( ( ) ( ) set ) -defined B : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) ;
:: original: .:
redefine func .: R -> ( ( Function-like V21( bool A : ( ( non empty partition-membered ) ( non empty partition-membered ) Element of bool (bool (bool B : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool B : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool A : ( ( non empty partition-membered ) ( non empty partition-membered ) Element of bool (bool (bool B : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool B : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) , bool B : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool B : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like bool A : ( ( non empty partition-membered ) ( non empty partition-membered ) Element of bool (bool (bool B : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool B : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool A : ( ( non empty partition-membered ) ( non empty partition-membered ) Element of bool (bool (bool B : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool B : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -defined bool B : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool B : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V21( bool A : ( ( non empty partition-membered ) ( non empty partition-membered ) Element of bool (bool (bool B : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool B : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool A : ( ( non empty partition-membered ) ( non empty partition-membered ) Element of bool (bool (bool B : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool B : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) , bool B : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool B : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) Function of bool A : ( ( non empty partition-membered ) ( non empty partition-membered ) Element of bool (bool (bool B : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool B : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool A : ( ( non empty partition-membered ) ( non empty partition-membered ) Element of bool (bool (bool B : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool B : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) , bool B : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool B : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ;
end;

theorem :: RELSET_2:22
for A, B being ( ( ) ( ) set )
for R being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) holds union ((.: R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like V21( bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) , bool b2 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b2 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b2 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b2 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V21( bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) , bool b2 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b2 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) Function of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) , bool b2 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b2 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) .: A : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of bool (bool b2 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) Element of bool (bool b2 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool b2 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) c= R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) .: (union A : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) Element of bool b2 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;

begin

definition
let A, B be ( ( ) ( ) set ) ;
let X be ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;
let R be ( ( ) ( Relation-like A : ( ( ) ( ) set ) -defined B : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) ;
func R .:^ X -> ( ( ) ( ) set ) equals :: RELSET_2:def 2
 Intersect ((.: R : ( ( ) ( ) set ) ) : ( ( Function-like V21( bool A : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool A : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) , bool B : ( ( non empty partition-membered ) ( non empty partition-membered ) Element of bool (bool (bool A : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool A : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool B : ( ( non empty partition-membered ) ( non empty partition-membered ) Element of bool (bool (bool A : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool A : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like bool A : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool A : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -defined bool B : ( ( non empty partition-membered ) ( non empty partition-membered ) Element of bool (bool (bool A : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool A : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool B : ( ( non empty partition-membered ) ( non empty partition-membered ) Element of bool (bool (bool A : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool A : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V21( bool A : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool A : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) , bool B : ( ( non empty partition-membered ) ( non empty partition-membered ) Element of bool (bool (bool A : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool A : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool B : ( ( non empty partition-membered ) ( non empty partition-membered ) Element of bool (bool (bool A : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool A : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) Function of bool A : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool A : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) , bool B : ( ( non empty partition-membered ) ( non empty partition-membered ) Element of bool (bool (bool A : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool A : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool B : ( ( non empty partition-membered ) ( non empty partition-membered ) Element of bool (bool (bool A : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool A : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) .: {_{X : ( ( ) ( ) a_partition of A : ( ( non empty ) ( non empty ) set ) ) }_} : ( ( ) ( ) a_partition of X : ( ( ) ( ) a_partition of A : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of bool (bool B : ( ( non empty partition-membered ) ( non empty partition-membered ) Element of bool (bool (bool A : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool A : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty ) Element of bool (bool B : ( ( non empty partition-membered ) ( non empty partition-membered ) Element of bool (bool (bool A : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool A : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool B : ( ( non empty partition-membered ) ( non empty partition-membered ) Element of bool (bool (bool A : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool A : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ;
end;

definition
let A, B be ( ( ) ( ) set ) ;
let X be ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;
let R be ( ( ) ( Relation-like A : ( ( ) ( ) set ) -defined B : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) ;
:: original: .:^
redefine func R .:^ X -> ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;
end;

theorem :: RELSET_2:23
for A, B being ( ( ) ( ) set )
for X being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for R being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) holds
( (.: R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like V21( bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) , bool b2 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b2 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b2 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b2 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V21( bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) , bool b2 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b2 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) Function of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) , bool b2 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b2 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) .: {_{X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) }_} : ( ( ) ( ) a_partition of b3 : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool (bool b2 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) Element of bool (bool b2 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) = {} : ( ( ) ( empty Relation-like non-empty empty-yielding ) set ) iff X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) = {} : ( ( ) ( empty Relation-like non-empty empty-yielding ) set ) ) ;

theorem :: RELSET_2:24
for A, B, y being ( ( ) ( ) set )
for X being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for R being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) st y : ( ( ) ( ) set ) in R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) .:^ X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds
for x being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) in X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds
y : ( ( ) ( ) set ) in Im (R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) ,x : ( ( ) ( ) set ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: RELSET_2:25
for B being ( ( non empty ) ( non empty ) set )
for A being ( ( ) ( ) set )
for X being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for y being ( ( ) ( ) Element of B : ( ( non empty ) ( non empty ) set ) )
for R being ( ( ) ( Relation-like b2 : ( ( ) ( ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) holds
( y : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) in R : ( ( ) ( Relation-like b2 : ( ( ) ( ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) .:^ X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) iff for x being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) in X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds
y : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) in Im (R : ( ( ) ( Relation-like b2 : ( ( ) ( ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) ,x : ( ( ) ( ) set ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) ;

theorem :: RELSET_2:26
for A, B being ( ( ) ( ) set )
for X1, X2 being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for R being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) st (.: R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like V21( bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) , bool b2 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b2 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b2 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b2 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V21( bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) , bool b2 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b2 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) Function of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) , bool b2 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b2 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) .: {_{X1 : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) }_} : ( ( ) ( ) a_partition of b3 : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool (bool b2 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) Element of bool (bool b2 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) = {} : ( ( ) ( empty Relation-like non-empty empty-yielding ) set ) holds
R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) .:^ (X1 : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) \/ X2 : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) = R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) .:^ X2 : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: RELSET_2:27
for A, B being ( ( ) ( ) set )
for X1, X2 being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for R being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) holds R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) .:^ (X1 : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) \/ X2 : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) = (R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) .:^ X1 : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) /\ (R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) .:^ X2 : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool b2 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: RELSET_2:28
for A being ( ( non empty ) ( non empty ) set )
for B being ( ( ) ( ) set )
for F being ( ( ) ( ) Subset-Family of )
for R being ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Relation of ,) holds { (R : ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Relation of ,) .:^ X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) where X is ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) in F : ( ( ) ( ) Subset-Family of ) } is ( ( ) ( ) Subset-Family of ) ;

theorem :: RELSET_2:29
for A, B being ( ( ) ( ) set )
for X being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for R being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) st X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) = {} : ( ( ) ( empty Relation-like non-empty empty-yielding ) set ) holds
R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) .:^ X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) = B : ( ( ) ( ) set ) ;

theorem :: RELSET_2:30
for A being ( ( ) ( ) set )
for B being ( ( non empty ) ( non empty ) set )
for R being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( non empty ) ( non empty ) set ) -valued ) Relation of ,)
for F being ( ( ) ( ) Subset-Family of )
for G being ( ( ) ( ) Subset-Family of ) st G : ( ( ) ( ) Subset-Family of ) = { (R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( non empty ) ( non empty ) set ) -valued ) Relation of ,) .:^ Y : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) where Y is ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : Y : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) in F : ( ( ) ( ) Subset-Family of ) } holds
R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( non empty ) ( non empty ) set ) -valued ) Relation of ,) .:^ (union F : ( ( ) ( ) Subset-Family of ) ) : ( ( ) ( ) Element of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) = Intersect G : ( ( ) ( ) Subset-Family of ) : ( ( ) ( ) Element of bool b2 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: RELSET_2:31
for A, B being ( ( ) ( ) set )
for X1, X2 being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for R being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) st X1 : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) c= X2 : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds
R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) .:^ X2 : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) c= R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) .:^ X1 : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: RELSET_2:32
for A, B being ( ( ) ( ) set )
for X1, X2 being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for R being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) holds (R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) .:^ X1 : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) \/ (R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) .:^ X2 : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool b2 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) c= R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) .:^ (X1 : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) /\ X2 : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: RELSET_2:33
for A, B being ( ( ) ( ) set )
for X being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for R1, R2 being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) holds (R1 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) /\ R2 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Element of bool [:b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) .:^ X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) = (R1 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) .:^ X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) /\ (R2 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) .:^ X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool b2 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: RELSET_2:34
for A, B being ( ( ) ( ) set )
for X being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for FR being ( ( ) ( ) Subset-Family of ) holds (union FR : ( ( ) ( ) Subset-Family of ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Element of bool [:b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) .: X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool b2 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = union { (R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) .: X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool b2 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) where R is ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) : R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) in FR : ( ( ) ( ) Subset-Family of ) } : ( ( ) ( ) set ) ;

theorem :: RELSET_2:35
for A, B being ( ( ) ( ) set )
for FR being ( ( ) ( ) Subset-Family of )
for A, B being ( ( ) ( ) set )
for X being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds { (R : ( ( ) ( Relation-like b4 : ( ( ) ( ) set ) -defined b5 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) .:^ X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) where R is ( ( ) ( Relation-like b4 : ( ( ) ( ) set ) -defined b5 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) : R : ( ( ) ( Relation-like b4 : ( ( ) ( ) set ) -defined b5 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) in FR : ( ( ) ( ) Subset-Family of ) } is ( ( ) ( ) Subset-Family of ) ;

theorem :: RELSET_2:36
for A, B being ( ( ) ( ) set )
for X being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for R being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) st R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) = {} : ( ( ) ( empty Relation-like non-empty empty-yielding ) set ) & X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) <> {} : ( ( ) ( empty Relation-like non-empty empty-yielding ) set ) holds
R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) .:^ X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) = {} : ( ( ) ( empty Relation-like non-empty empty-yielding ) set ) ;

theorem :: RELSET_2:37
for A, B being ( ( ) ( ) set )
for X being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for R being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) st R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) = [:A : ( ( ) ( ) set ) ,B : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) holds
R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) .:^ X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) = B : ( ( ) ( ) set ) ;

theorem :: RELSET_2:38
for B, A being ( ( ) ( ) set )
for X being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for FR being ( ( ) ( ) Subset-Family of )
for G being ( ( ) ( ) Subset-Family of ) st G : ( ( ) ( ) Subset-Family of ) = { (R : ( ( ) ( Relation-like b2 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) .:^ X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) where R is ( ( ) ( Relation-like b2 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) : R : ( ( ) ( Relation-like b2 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) in FR : ( ( ) ( ) Subset-Family of ) } holds
(Intersect FR : ( ( ) ( ) Subset-Family of ) ) : ( ( ) ( Relation-like b2 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Element of bool [:b2 : ( ( ) ( ) set ) ,b1 : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) .:^ X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) = Intersect G : ( ( ) ( ) Subset-Family of ) : ( ( ) ( ) Element of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: RELSET_2:39
for A, B being ( ( ) ( ) set )
for X being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for R1, R2 being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) st R1 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) c= R2 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) holds
R1 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) .:^ X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) c= R2 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) .:^ X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: RELSET_2:40
for A, B being ( ( ) ( ) set )
for X being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for R1, R2 being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) holds (R1 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) .:^ X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) \/ (R2 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) .:^ X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool b2 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) c= (R1 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) \/ R2 : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Element of bool [:b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) .:^ X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: RELSET_2:41
for y, x, A, B being ( ( ) ( ) set )
for R being ( ( ) ( Relation-like b3 : ( ( ) ( ) set ) -defined b4 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) holds
( y : ( ( ) ( ) set ) in Im ((R : ( ( ) ( Relation-like b3 : ( ( ) ( ) set ) -defined b4 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) `) : ( ( ) ( Relation-like b3 : ( ( ) ( ) set ) -defined b4 : ( ( ) ( ) set ) -valued ) Element of bool [:b3 : ( ( ) ( ) set ) ,b4 : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ,x : ( ( ) ( ) set ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) iff ( not [x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) ] : ( ( ) ( V18() ) set ) in R : ( ( ) ( Relation-like b3 : ( ( ) ( ) set ) -defined b4 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) & x : ( ( ) ( ) set ) in A : ( ( ) ( ) set ) & y : ( ( ) ( ) set ) in B : ( ( ) ( ) set ) ) ) ;

theorem :: RELSET_2:42
for A, B being ( ( ) ( ) set )
for X being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for R being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) st X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) <> {} : ( ( ) ( empty Relation-like non-empty empty-yielding ) set ) holds
R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) .:^ X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) c= R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) .: X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool b2 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: RELSET_2:43
for A, B being ( ( ) ( ) set )
for R being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) )
for X, Y being ( ( ) ( ) set ) holds
( X : ( ( ) ( ) set ) meets (R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) ~) : ( ( ) ( Relation-like b2 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Element of bool [:b2 : ( ( ) ( ) set ) ,b1 : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) .: Y : ( ( ) ( ) set ) : ( ( ) ( ) Element of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) iff ex x, y being ( ( ) ( ) set ) st
( x : ( ( ) ( ) set ) in X : ( ( ) ( ) set ) & y : ( ( ) ( ) set ) in Y : ( ( ) ( ) set ) & x : ( ( ) ( ) set ) in Im ((R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) ~) : ( ( ) ( Relation-like b2 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Element of bool [:b2 : ( ( ) ( ) set ) ,b1 : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) set ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) ) ;

theorem :: RELSET_2:44
for A, B being ( ( ) ( ) set )
for R being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) )
for X, Y being ( ( ) ( ) set ) holds
( ex x, y being ( ( ) ( ) set ) st
( x : ( ( ) ( ) set ) in X : ( ( ) ( ) set ) & y : ( ( ) ( ) set ) in Y : ( ( ) ( ) set ) & x : ( ( ) ( ) set ) in Im ((R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) ~) : ( ( ) ( Relation-like b2 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Element of bool [:b2 : ( ( ) ( ) set ) ,b1 : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) set ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) iff Y : ( ( ) ( ) set ) meets R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) .: X : ( ( ) ( ) set ) : ( ( ) ( ) Element of bool b2 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: RELSET_2:45
for A, B being ( ( ) ( ) set )
for X being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for Y being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for R being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) holds
( X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) misses (R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) ~) : ( ( ) ( Relation-like b2 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Element of bool [:b2 : ( ( ) ( ) set ) ,b1 : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) .: Y : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) iff Y : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) misses R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) .: X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool b2 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: RELSET_2:46
for A, B being ( ( ) ( ) set )
for R being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) )
for X being ( ( ) ( ) set ) holds R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) .: X : ( ( ) ( ) set ) : ( ( ) ( ) Element of bool b2 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) .: (X : ( ( ) ( ) set ) /\ (proj1 R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) Element of bool b2 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: RELSET_2:47
for A, B being ( ( ) ( ) set )
for R being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) )
for Y being ( ( ) ( ) set ) holds (R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) ~) : ( ( ) ( Relation-like b2 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Element of bool [:b2 : ( ( ) ( ) set ) ,b1 : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) .: Y : ( ( ) ( ) set ) : ( ( ) ( ) Element of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = (R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) ~) : ( ( ) ( Relation-like b2 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Element of bool [:b2 : ( ( ) ( ) set ) ,b1 : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) .: (Y : ( ( ) ( ) set ) /\ (proj2 R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) Element of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: RELSET_2:48
for A, B being ( ( ) ( ) set )
for X being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for R being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) holds (R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) .:^ X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ` : ( ( ) ( ) Element of bool b2 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = (R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) `) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Element of bool [:b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) .: X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool b2 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;

definition
let A, B, C be ( ( ) ( ) set ) ;
let R be ( ( ) ( Relation-like A : ( ( ) ( ) set ) -defined B : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) ;
let S be ( ( ) ( Relation-like B : ( ( ) ( ) set ) -defined C : ( ( ) ( ) set ) -valued ) Subset of ( ( ) ( non empty ) set ) ) ;
:: original: *
redefine func R * S -> ( ( ) ( Relation-like A : ( ( non empty ) ( non empty ) set ) -defined C : ( ( ) ( ) a_partition of A : ( ( non empty ) ( non empty ) set ) ) -valued ) Relation of ,) ;
end;

theorem :: RELSET_2:49
for A, B being ( ( ) ( ) set )
for X being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for R being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Relation of ,) holds (R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Relation of ,) .: X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool b2 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ` : ( ( ) ( ) Element of bool b2 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = (R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Relation of ,) `) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Element of bool [:b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) .:^ X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: RELSET_2:50
for B, A being ( ( ) ( ) set )
for R being ( ( ) ( Relation-like b2 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Relation of ,) holds
( proj1 R : ( ( ) ( Relation-like b2 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Relation of ,) : ( ( ) ( ) set ) = (R : ( ( ) ( Relation-like b2 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Relation of ,) ~) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Element of bool [:b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) .: B : ( ( ) ( ) set ) : ( ( ) ( ) Element of bool b2 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) & proj2 R : ( ( ) ( Relation-like b2 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Relation of ,) : ( ( ) ( ) set ) = R : ( ( ) ( Relation-like b2 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Relation of ,) .: A : ( ( ) ( ) set ) : ( ( ) ( ) Element of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: RELSET_2:51
for A, B, C being ( ( ) ( ) set )
for R being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Relation of ,)
for S being ( ( ) ( Relation-like b2 : ( ( ) ( ) set ) -defined b3 : ( ( ) ( ) set ) -valued ) Relation of ,) holds
( proj1 (R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Relation of ,) * S : ( ( ) ( Relation-like b2 : ( ( ) ( ) set ) -defined b3 : ( ( ) ( ) set ) -valued ) Relation of ,) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b3 : ( ( ) ( ) set ) -valued ) Relation of ,) : ( ( ) ( ) set ) = (R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Relation of ,) ~) : ( ( ) ( Relation-like b2 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Element of bool [:b2 : ( ( ) ( ) set ) ,b1 : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) .: (proj1 S : ( ( ) ( Relation-like b2 : ( ( ) ( ) set ) -defined b3 : ( ( ) ( ) set ) -valued ) Relation of ,) ) : ( ( ) ( ) set ) : ( ( ) ( ) Element of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) & proj1 (R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Relation of ,) * S : ( ( ) ( Relation-like b2 : ( ( ) ( ) set ) -defined b3 : ( ( ) ( ) set ) -valued ) Relation of ,) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b3 : ( ( ) ( ) set ) -valued ) Relation of ,) : ( ( ) ( ) set ) c= proj1 R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Relation of ,) : ( ( ) ( ) set ) ) ;

theorem :: RELSET_2:52
for A, B, C being ( ( ) ( ) set )
for R being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Relation of ,)
for S being ( ( ) ( Relation-like b2 : ( ( ) ( ) set ) -defined b3 : ( ( ) ( ) set ) -valued ) Relation of ,) holds
( proj2 (R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Relation of ,) * S : ( ( ) ( Relation-like b2 : ( ( ) ( ) set ) -defined b3 : ( ( ) ( ) set ) -valued ) Relation of ,) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b3 : ( ( ) ( ) set ) -valued ) Relation of ,) : ( ( ) ( ) set ) = S : ( ( ) ( Relation-like b2 : ( ( ) ( ) set ) -defined b3 : ( ( ) ( ) set ) -valued ) Relation of ,) .: (proj2 R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Relation of ,) ) : ( ( ) ( ) set ) : ( ( ) ( ) Element of bool b3 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) & proj2 (R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Relation of ,) * S : ( ( ) ( Relation-like b2 : ( ( ) ( ) set ) -defined b3 : ( ( ) ( ) set ) -valued ) Relation of ,) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b3 : ( ( ) ( ) set ) -valued ) Relation of ,) : ( ( ) ( ) set ) c= proj2 S : ( ( ) ( Relation-like b2 : ( ( ) ( ) set ) -defined b3 : ( ( ) ( ) set ) -valued ) Relation of ,) : ( ( ) ( ) set ) ) ;

theorem :: RELSET_2:53
for A, B being ( ( ) ( ) set )
for X being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for R being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Relation of ,) holds
( X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) c= proj1 R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Relation of ,) : ( ( ) ( ) set ) iff X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) c= (R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Relation of ,) * (R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Relation of ,) ~) : ( ( ) ( Relation-like b2 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Element of bool [:b2 : ( ( ) ( ) set ) ,b1 : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Relation of ,) .: X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: RELSET_2:54
for A, B being ( ( ) ( ) set )
for Y being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for R being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Relation of ,) holds
( Y : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) c= proj2 R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Relation of ,) : ( ( ) ( ) set ) iff Y : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) c= ((R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Relation of ,) ~) : ( ( ) ( Relation-like b2 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Element of bool [:b2 : ( ( ) ( ) set ) ,b1 : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) * R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Relation of ,) ) : ( ( ) ( Relation-like b2 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Relation of ,) .: Y : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool b2 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: RELSET_2:55
for B, A being ( ( ) ( ) set )
for R being ( ( ) ( Relation-like b2 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Relation of ,) holds
( proj1 R : ( ( ) ( Relation-like b2 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Relation of ,) : ( ( ) ( ) set ) = (R : ( ( ) ( Relation-like b2 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Relation of ,) ~) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Element of bool [:b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) .: B : ( ( ) ( ) set ) : ( ( ) ( ) Element of bool b2 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) & (R : ( ( ) ( Relation-like b2 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Relation of ,) ~) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Element of bool [:b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) .: (R : ( ( ) ( Relation-like b2 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Relation of ,) .: A : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool b2 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = (R : ( ( ) ( Relation-like b2 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Relation of ,) ~) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Element of bool [:b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) .: (proj2 R : ( ( ) ( Relation-like b2 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Relation of ,) ) : ( ( ) ( ) set ) : ( ( ) ( ) Element of bool b2 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: RELSET_2:56
for B, A being ( ( ) ( ) set )
for R being ( ( ) ( Relation-like b2 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Relation of ,) holds (R : ( ( ) ( Relation-like b2 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Relation of ,) ~) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Element of bool [:b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) .: B : ( ( ) ( ) set ) : ( ( ) ( ) Element of bool b2 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = (R : ( ( ) ( Relation-like b2 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Relation of ,) * (R : ( ( ) ( Relation-like b2 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Relation of ,) ~) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Element of bool [:b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like b2 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Relation of ,) .: A : ( ( ) ( ) set ) : ( ( ) ( ) Element of bool b2 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: RELSET_2:57
for A, B being ( ( ) ( ) set )
for R being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Relation of ,) holds R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Relation of ,) .: A : ( ( ) ( ) set ) : ( ( ) ( ) Element of bool b2 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = ((R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Relation of ,) ~) : ( ( ) ( Relation-like b2 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Element of bool [:b2 : ( ( ) ( ) set ) ,b1 : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) * R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Relation of ,) ) : ( ( ) ( Relation-like b2 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Relation of ,) .: B : ( ( ) ( ) set ) : ( ( ) ( ) Element of bool b2 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: RELSET_2:58
for A, B, C being ( ( ) ( ) set )
for X being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for R being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Relation of ,)
for S being ( ( ) ( Relation-like b2 : ( ( ) ( ) set ) -defined b3 : ( ( ) ( ) set ) -valued ) Relation of ,) holds S : ( ( ) ( Relation-like b2 : ( ( ) ( ) set ) -defined b3 : ( ( ) ( ) set ) -valued ) Relation of ,) .:^ (R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Relation of ,) .: X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool b2 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) = ((R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Relation of ,) * (S : ( ( ) ( Relation-like b2 : ( ( ) ( ) set ) -defined b3 : ( ( ) ( ) set ) -valued ) Relation of ,) `) : ( ( ) ( Relation-like b2 : ( ( ) ( ) set ) -defined b3 : ( ( ) ( ) set ) -valued ) Element of bool [:b2 : ( ( ) ( ) set ) ,b3 : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b3 : ( ( ) ( ) set ) -valued ) Relation of ,) `) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b3 : ( ( ) ( ) set ) -valued ) Element of bool [:b1 : ( ( ) ( ) set ) ,b3 : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) .:^ X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: RELSET_2:59
for A, B being ( ( ) ( ) set )
for R being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Relation of ,) holds (R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Relation of ,) `) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Element of bool [:b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ~ : ( ( ) ( Relation-like b2 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Element of bool [:b2 : ( ( ) ( ) set ) ,b1 : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) = (R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Relation of ,) ~) : ( ( ) ( Relation-like b2 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Element of bool [:b2 : ( ( ) ( ) set ) ,b1 : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ` : ( ( ) ( Relation-like b2 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Element of bool [:b2 : ( ( ) ( ) set ) ,b1 : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: RELSET_2:60
for A, B being ( ( ) ( ) set )
for X being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for Y being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for R being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Relation of ,) holds
( X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) c= (R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Relation of ,) ~) : ( ( ) ( Relation-like b2 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Element of bool [:b2 : ( ( ) ( ) set ) ,b1 : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) .:^ Y : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) iff Y : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) c= R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Relation of ,) .:^ X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) ;

theorem :: RELSET_2:61
for A, B being ( ( ) ( ) set )
for X being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for Y being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for R being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Relation of ,) holds
( R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Relation of ,) .: (X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) `) : ( ( ) ( ) Element of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool b2 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) c= Y : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ` : ( ( ) ( ) Element of bool b2 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) iff (R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Relation of ,) ~) : ( ( ) ( Relation-like b2 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Element of bool [:b2 : ( ( ) ( ) set ) ,b1 : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) .: Y : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) c= X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) ;

theorem :: RELSET_2:62
for A, B being ( ( ) ( ) set )
for X being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for Y being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for R being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Relation of ,) holds
( X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) c= (R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Relation of ,) ~) : ( ( ) ( Relation-like b2 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Element of bool [:b2 : ( ( ) ( ) set ) ,b1 : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) .:^ (R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Relation of ,) .:^ X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) & Y : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) c= R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Relation of ,) .:^ ((R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Relation of ,) ~) : ( ( ) ( Relation-like b2 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Element of bool [:b2 : ( ( ) ( ) set ) ,b1 : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) .:^ Y : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) ;

theorem :: RELSET_2:63
for A, B being ( ( ) ( ) set )
for X being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for Y being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for R being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Relation of ,) holds
( R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Relation of ,) .:^ X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) = R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Relation of ,) .:^ ((R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Relation of ,) ~) : ( ( ) ( Relation-like b2 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Element of bool [:b2 : ( ( ) ( ) set ) ,b1 : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) .:^ (R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Relation of ,) .:^ X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) & (R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Relation of ,) ~) : ( ( ) ( Relation-like b2 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Element of bool [:b2 : ( ( ) ( ) set ) ,b1 : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) .:^ Y : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) = (R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Relation of ,) ~) : ( ( ) ( Relation-like b2 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Element of bool [:b2 : ( ( ) ( ) set ) ,b1 : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) .:^ (R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Relation of ,) .:^ ((R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Relation of ,) ~) : ( ( ) ( Relation-like b2 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) Element of bool [:b2 : ( ( ) ( ) set ) ,b1 : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) .:^ Y : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) ;

theorem :: RELSET_2:64
for A, B being ( ( ) ( ) set )
for R being ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Relation of ,) holds (id A : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued V24() V26() V27() V31() ) set ) * R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Relation of ,) : ( ( Relation-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) set ) = R : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) Relation of ,) * (id B : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like b2 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued V24() V26() V27() V31() ) set ) : ( ( Relation-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) set ) ;