:: SYSREL semantic presentation

begin

theorem :: SYSREL:1
for X, Y being ( ( ) ( ) set )
for R being ( ( Relation-like ) ( Relation-like ) Relation) holds
( dom (R : ( ( Relation-like ) ( Relation-like ) Relation) /\ [:X : ( ( ) ( ) set ) ,Y : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) c= X : ( ( ) ( ) set ) & rng (R : ( ( Relation-like ) ( Relation-like ) Relation) /\ [:X : ( ( ) ( ) set ) ,Y : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) c= Y : ( ( ) ( ) set ) ) ;

theorem :: SYSREL:2
for X, Y being ( ( ) ( ) set )
for R being ( ( Relation-like ) ( Relation-like ) Relation) st X : ( ( ) ( ) set ) misses Y : ( ( ) ( ) set ) holds
dom (R : ( ( Relation-like ) ( Relation-like ) Relation) /\ [:X : ( ( ) ( ) set ) ,Y : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) misses rng (R : ( ( Relation-like ) ( Relation-like ) Relation) /\ [:X : ( ( ) ( ) set ) ,Y : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ;

theorem :: SYSREL:3
for X, Y being ( ( ) ( ) set )
for R being ( ( Relation-like ) ( Relation-like ) Relation) st R : ( ( Relation-like ) ( Relation-like ) Relation) c= [:X : ( ( ) ( ) set ) ,Y : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) holds
( dom R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) c= X : ( ( ) ( ) set ) & rng R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) c= Y : ( ( ) ( ) set ) ) ;

theorem :: SYSREL:4
for X, Y being ( ( ) ( ) set )
for R being ( ( Relation-like ) ( Relation-like ) Relation) st R : ( ( Relation-like ) ( Relation-like ) Relation) c= [:X : ( ( ) ( ) set ) ,Y : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) holds
R : ( ( Relation-like ) ( Relation-like ) Relation) ~ : ( ( Relation-like ) ( Relation-like ) set ) c= [:Y : ( ( ) ( ) set ) ,X : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) ;

theorem :: SYSREL:5
for X, Y being ( ( ) ( ) set ) holds [:X : ( ( ) ( ) set ) ,Y : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) ~ : ( ( Relation-like ) ( Relation-like ) set ) = [:Y : ( ( ) ( ) set ) ,X : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) ;

theorem :: SYSREL:6
for R, S, T being ( ( Relation-like ) ( Relation-like ) Relation) holds (R : ( ( Relation-like ) ( Relation-like ) Relation) \/ S : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( Relation-like ) set ) * T : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( Relation-like ) ( Relation-like ) set ) = (R : ( ( Relation-like ) ( Relation-like ) Relation) * T : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) set ) \/ (S : ( ( Relation-like ) ( Relation-like ) Relation) * T : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) set ) : ( ( ) ( Relation-like ) set ) ;

theorem :: SYSREL:7
for X, Y, x, y being ( ( ) ( ) set )
for R being ( ( Relation-like ) ( Relation-like ) Relation) holds
( ( X : ( ( ) ( ) set ) misses Y : ( ( ) ( ) set ) & R : ( ( Relation-like ) ( Relation-like ) Relation) c= [:X : ( ( ) ( ) set ) ,Y : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) \/ [:Y : ( ( ) ( ) set ) ,X : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( Relation-like ) set ) & [x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) ] : ( ( ) ( ) set ) in R : ( ( Relation-like ) ( Relation-like ) Relation) & x : ( ( ) ( ) set ) in X : ( ( ) ( ) set ) implies ( not x : ( ( ) ( ) set ) in Y : ( ( ) ( ) set ) & not y : ( ( ) ( ) set ) in X : ( ( ) ( ) set ) & y : ( ( ) ( ) set ) in Y : ( ( ) ( ) set ) ) ) & ( X : ( ( ) ( ) set ) misses Y : ( ( ) ( ) set ) & R : ( ( Relation-like ) ( Relation-like ) Relation) c= [:X : ( ( ) ( ) set ) ,Y : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) \/ [:Y : ( ( ) ( ) set ) ,X : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( Relation-like ) set ) & [x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) ] : ( ( ) ( ) set ) in R : ( ( Relation-like ) ( Relation-like ) Relation) & y : ( ( ) ( ) set ) in Y : ( ( ) ( ) set ) implies ( not y : ( ( ) ( ) set ) in X : ( ( ) ( ) set ) & not x : ( ( ) ( ) set ) in Y : ( ( ) ( ) set ) & x : ( ( ) ( ) set ) in X : ( ( ) ( ) set ) ) ) & ( X : ( ( ) ( ) set ) misses Y : ( ( ) ( ) set ) & R : ( ( Relation-like ) ( Relation-like ) Relation) c= [:X : ( ( ) ( ) set ) ,Y : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) \/ [:Y : ( ( ) ( ) set ) ,X : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( Relation-like ) set ) & [x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) ] : ( ( ) ( ) set ) in R : ( ( Relation-like ) ( Relation-like ) Relation) & x : ( ( ) ( ) set ) in Y : ( ( ) ( ) set ) implies ( not x : ( ( ) ( ) set ) in X : ( ( ) ( ) set ) & not y : ( ( ) ( ) set ) in Y : ( ( ) ( ) set ) & y : ( ( ) ( ) set ) in X : ( ( ) ( ) set ) ) ) & ( X : ( ( ) ( ) set ) misses Y : ( ( ) ( ) set ) & R : ( ( Relation-like ) ( Relation-like ) Relation) c= [:X : ( ( ) ( ) set ) ,Y : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) \/ [:Y : ( ( ) ( ) set ) ,X : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( Relation-like ) set ) & [x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) ] : ( ( ) ( ) set ) in R : ( ( Relation-like ) ( Relation-like ) Relation) & y : ( ( ) ( ) set ) in X : ( ( ) ( ) set ) implies ( not x : ( ( ) ( ) set ) in X : ( ( ) ( ) set ) & not y : ( ( ) ( ) set ) in Y : ( ( ) ( ) set ) & x : ( ( ) ( ) set ) in Y : ( ( ) ( ) set ) ) ) ) ;

theorem :: SYSREL:8
for X, Y, Z being ( ( ) ( ) set )
for R being ( ( Relation-like ) ( Relation-like ) Relation) st R : ( ( Relation-like ) ( Relation-like ) Relation) c= [:X : ( ( ) ( ) set ) ,Y : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) holds
( R : ( ( Relation-like ) ( Relation-like ) Relation) | Z : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like ) set ) = R : ( ( Relation-like ) ( Relation-like ) Relation) /\ [:Z : ( ( ) ( ) set ) ,Y : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( Relation-like ) set ) & Z : ( ( ) ( ) set ) |` R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( Relation-like ) ( Relation-like ) set ) = R : ( ( Relation-like ) ( Relation-like ) Relation) /\ [:X : ( ( ) ( ) set ) ,Z : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( Relation-like ) set ) ) ;

theorem :: SYSREL:9
for X, Y, Z, W being ( ( ) ( ) set )
for R being ( ( Relation-like ) ( Relation-like ) Relation) st R : ( ( Relation-like ) ( Relation-like ) Relation) c= [:X : ( ( ) ( ) set ) ,Y : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) & X : ( ( ) ( ) set ) = Z : ( ( ) ( ) set ) \/ W : ( ( ) ( ) set ) : ( ( ) ( ) set ) holds
R : ( ( Relation-like ) ( Relation-like ) Relation) = (R : ( ( Relation-like ) ( Relation-like ) Relation) | Z : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like ) set ) \/ (R : ( ( Relation-like ) ( Relation-like ) Relation) | W : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like ) set ) : ( ( ) ( Relation-like ) set ) ;

theorem :: SYSREL:10
for X, Y being ( ( ) ( ) set )
for R being ( ( Relation-like ) ( Relation-like ) Relation) st X : ( ( ) ( ) set ) misses Y : ( ( ) ( ) set ) & R : ( ( Relation-like ) ( Relation-like ) Relation) c= [:X : ( ( ) ( ) set ) ,Y : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) \/ [:Y : ( ( ) ( ) set ) ,X : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( Relation-like ) set ) holds
R : ( ( Relation-like ) ( Relation-like ) Relation) | X : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like ) set ) c= [:X : ( ( ) ( ) set ) ,Y : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) ;

theorem :: SYSREL:11
for R, S being ( ( Relation-like ) ( Relation-like ) Relation) st R : ( ( Relation-like ) ( Relation-like ) Relation) c= S : ( ( Relation-like ) ( Relation-like ) Relation) holds
R : ( ( Relation-like ) ( Relation-like ) Relation) ~ : ( ( Relation-like ) ( Relation-like ) set ) c= S : ( ( Relation-like ) ( Relation-like ) Relation) ~ : ( ( Relation-like ) ( Relation-like ) set ) ;

theorem :: SYSREL:12
for X being ( ( ) ( ) set ) holds (id X : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) set ) * (id X : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) set ) : ( ( Relation-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) set ) = id X : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) set ) ;

theorem :: SYSREL:13
for x being ( ( ) ( ) set ) holds id {x : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) : ( ( Relation-like ) ( Relation-like {b1 : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) -defined {b1 : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) -valued ) set ) = {[x : ( ( ) ( ) set ) ,x : ( ( ) ( ) set ) ] : ( ( ) ( ) set ) } : ( ( ) ( non empty Relation-like ) set ) ;

theorem :: SYSREL:14
for X, Y being ( ( ) ( ) set ) holds
( id (X : ( ( ) ( ) set ) \/ Y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like b1 : ( ( ) ( ) set ) \/ b2 : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) \/ b2 : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued ) set ) = (id X : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) set ) \/ (id Y : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like b2 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) set ) : ( ( ) ( Relation-like ) set ) & id (X : ( ( ) ( ) set ) /\ Y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like b1 : ( ( ) ( ) set ) /\ b2 : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) /\ b2 : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued ) set ) = (id X : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) set ) /\ (id Y : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like b2 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) set ) : ( ( ) ( Relation-like ) set ) & id (X : ( ( ) ( ) set ) \ Y : ( ( ) ( ) set ) ) : ( ( ) ( ) M2( bool b1 : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) : ( ( Relation-like ) ( Relation-like b1 : ( ( ) ( ) set ) \ b2 : ( ( ) ( ) set ) : ( ( ) ( ) M2( bool b1 : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) -defined b1 : ( ( ) ( ) set ) \ b2 : ( ( ) ( ) set ) : ( ( ) ( ) M2( bool b1 : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) -valued ) set ) = (id X : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) set ) \ (id Y : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like b2 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) set ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) M2( bool (id b1 : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) set ) : ( ( ) ( ) set ) )) ) ;

theorem :: SYSREL:15
for X, Y being ( ( ) ( ) set ) st X : ( ( ) ( ) set ) c= Y : ( ( ) ( ) set ) holds
id X : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) set ) c= id Y : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like b2 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) set ) -valued ) set ) ;

theorem :: SYSREL:16
for X, Y being ( ( ) ( ) set ) holds (id (X : ( ( ) ( ) set ) \ Y : ( ( ) ( ) set ) ) : ( ( ) ( ) M2( bool b1 : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) ) : ( ( Relation-like ) ( Relation-like b1 : ( ( ) ( ) set ) \ b2 : ( ( ) ( ) set ) : ( ( ) ( ) M2( bool b1 : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) -defined b1 : ( ( ) ( ) set ) \ b2 : ( ( ) ( ) set ) : ( ( ) ( ) M2( bool b1 : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) -valued ) set ) \ (id X : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) set ) : ( ( ) ( Relation-like b1 : ( ( ) ( ) set ) \ b2 : ( ( ) ( ) set ) : ( ( ) ( ) M2( bool b1 : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) -defined b1 : ( ( ) ( ) set ) \ b2 : ( ( ) ( ) set ) : ( ( ) ( ) M2( bool b1 : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) -valued ) M2( bool (id (b1 : ( ( ) ( ) set ) \ b2 : ( ( ) ( ) set ) ) : ( ( ) ( ) M2( bool b1 : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) ) : ( ( Relation-like ) ( Relation-like b1 : ( ( ) ( ) set ) \ b2 : ( ( ) ( ) set ) : ( ( ) ( ) M2( bool b1 : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) -defined b1 : ( ( ) ( ) set ) \ b2 : ( ( ) ( ) set ) : ( ( ) ( ) M2( bool b1 : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) -valued ) set ) : ( ( ) ( ) set ) )) = {} : ( ( ) ( empty Relation-like non-empty empty-yielding ) set ) ;

theorem :: SYSREL:17
for R being ( ( Relation-like ) ( Relation-like ) Relation) st R : ( ( Relation-like ) ( Relation-like ) Relation) c= id (dom R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like dom b1 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -defined dom b1 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -valued ) set ) holds
R : ( ( Relation-like ) ( Relation-like ) Relation) = id (dom R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like dom b1 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -defined dom b1 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -valued ) set ) ;

theorem :: SYSREL:18
for X being ( ( ) ( ) set )
for R being ( ( Relation-like ) ( Relation-like ) Relation) st id X : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) set ) c= R : ( ( Relation-like ) ( Relation-like ) Relation) \/ (R : ( ( Relation-like ) ( Relation-like ) Relation) ~) : ( ( Relation-like ) ( Relation-like ) set ) : ( ( ) ( Relation-like ) set ) holds
( id X : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) set ) c= R : ( ( Relation-like ) ( Relation-like ) Relation) & id X : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) set ) c= R : ( ( Relation-like ) ( Relation-like ) Relation) ~ : ( ( Relation-like ) ( Relation-like ) set ) ) ;

theorem :: SYSREL:19
for X being ( ( ) ( ) set )
for R being ( ( Relation-like ) ( Relation-like ) Relation) st id X : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) set ) c= R : ( ( Relation-like ) ( Relation-like ) Relation) holds
id X : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) set ) c= R : ( ( Relation-like ) ( Relation-like ) Relation) ~ : ( ( Relation-like ) ( Relation-like ) set ) ;

theorem :: SYSREL:20
for X being ( ( ) ( ) set )
for R being ( ( Relation-like ) ( Relation-like ) Relation) st R : ( ( Relation-like ) ( Relation-like ) Relation) c= [:X : ( ( ) ( ) set ) ,X : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) holds
( R : ( ( Relation-like ) ( Relation-like ) Relation) \ (id (dom R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like dom b2 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -defined dom b2 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -valued ) set ) : ( ( ) ( Relation-like ) M2( bool b2 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) )) = R : ( ( Relation-like ) ( Relation-like ) Relation) \ (id X : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) set ) : ( ( ) ( Relation-like ) M2( bool b2 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) )) & R : ( ( Relation-like ) ( Relation-like ) Relation) \ (id (rng R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like rng b2 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -defined rng b2 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -valued ) set ) : ( ( ) ( Relation-like ) M2( bool b2 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) )) = R : ( ( Relation-like ) ( Relation-like ) Relation) \ (id X : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) set ) : ( ( ) ( Relation-like ) M2( bool b2 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) )) ) ;

theorem :: SYSREL:21
for X being ( ( ) ( ) set )
for R being ( ( Relation-like ) ( Relation-like ) Relation) holds
( ( (id X : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) set ) * (R : ( ( Relation-like ) ( Relation-like ) Relation) \ (id X : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) set ) ) : ( ( ) ( Relation-like ) M2( bool b2 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) )) : ( ( Relation-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined ) set ) = {} : ( ( ) ( empty Relation-like non-empty empty-yielding ) set ) implies dom (R : ( ( Relation-like ) ( Relation-like ) Relation) \ (id X : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) set ) ) : ( ( ) ( Relation-like ) M2( bool b2 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) = (dom R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) \ X : ( ( ) ( ) set ) : ( ( ) ( ) M2( bool (dom b2 : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) ) & ( (R : ( ( Relation-like ) ( Relation-like ) Relation) \ (id X : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) set ) ) : ( ( ) ( Relation-like ) M2( bool b2 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) )) * (id X : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) set ) : ( ( Relation-like ) ( Relation-like b1 : ( ( ) ( ) set ) -valued ) set ) = {} : ( ( ) ( empty Relation-like non-empty empty-yielding ) set ) implies rng (R : ( ( Relation-like ) ( Relation-like ) Relation) \ (id X : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) set ) ) : ( ( ) ( Relation-like ) M2( bool b2 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) = (rng R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) \ X : ( ( ) ( ) set ) : ( ( ) ( ) M2( bool (rng b2 : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) ) ) ;

theorem :: SYSREL:22
for R being ( ( Relation-like ) ( Relation-like ) Relation) holds
( ( R : ( ( Relation-like ) ( Relation-like ) Relation) c= R : ( ( Relation-like ) ( Relation-like ) Relation) * R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( Relation-like ) ( Relation-like ) set ) & R : ( ( Relation-like ) ( Relation-like ) Relation) * (R : ( ( Relation-like ) ( Relation-like ) Relation) \ (id (rng R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like rng b1 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -defined rng b1 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -valued ) set ) ) : ( ( ) ( Relation-like ) M2( bool b1 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) )) : ( ( Relation-like ) ( Relation-like ) set ) = {} : ( ( ) ( empty Relation-like non-empty empty-yielding ) set ) implies id (rng R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like rng b1 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -defined rng b1 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -valued ) set ) c= R : ( ( Relation-like ) ( Relation-like ) Relation) ) & ( R : ( ( Relation-like ) ( Relation-like ) Relation) c= R : ( ( Relation-like ) ( Relation-like ) Relation) * R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( Relation-like ) ( Relation-like ) set ) & (R : ( ( Relation-like ) ( Relation-like ) Relation) \ (id (dom R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like dom b1 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -defined dom b1 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -valued ) set ) ) : ( ( ) ( Relation-like ) M2( bool b1 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) )) * R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( Relation-like ) ( Relation-like ) set ) = {} : ( ( ) ( empty Relation-like non-empty empty-yielding ) set ) implies id (dom R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like dom b1 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -defined dom b1 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -valued ) set ) c= R : ( ( Relation-like ) ( Relation-like ) Relation) ) ) ;

theorem :: SYSREL:23
for R being ( ( Relation-like ) ( Relation-like ) Relation) holds
( ( R : ( ( Relation-like ) ( Relation-like ) Relation) c= R : ( ( Relation-like ) ( Relation-like ) Relation) * R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( Relation-like ) ( Relation-like ) set ) & R : ( ( Relation-like ) ( Relation-like ) Relation) * (R : ( ( Relation-like ) ( Relation-like ) Relation) \ (id (rng R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like rng b1 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -defined rng b1 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -valued ) set ) ) : ( ( ) ( Relation-like ) M2( bool b1 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) )) : ( ( Relation-like ) ( Relation-like ) set ) = {} : ( ( ) ( empty Relation-like non-empty empty-yielding ) set ) implies R : ( ( Relation-like ) ( Relation-like ) Relation) /\ (id (rng R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like rng b1 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -defined rng b1 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -valued ) set ) : ( ( ) ( Relation-like ) set ) = id (rng R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like rng b1 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -defined rng b1 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -valued ) set ) ) & ( R : ( ( Relation-like ) ( Relation-like ) Relation) c= R : ( ( Relation-like ) ( Relation-like ) Relation) * R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( Relation-like ) ( Relation-like ) set ) & (R : ( ( Relation-like ) ( Relation-like ) Relation) \ (id (dom R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like dom b1 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -defined dom b1 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -valued ) set ) ) : ( ( ) ( Relation-like ) M2( bool b1 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) )) * R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( Relation-like ) ( Relation-like ) set ) = {} : ( ( ) ( empty Relation-like non-empty empty-yielding ) set ) implies R : ( ( Relation-like ) ( Relation-like ) Relation) /\ (id (dom R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like dom b1 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -defined dom b1 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -valued ) set ) : ( ( ) ( Relation-like ) set ) = id (dom R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like dom b1 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -defined dom b1 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -valued ) set ) ) ) ;

theorem :: SYSREL:24
for X being ( ( ) ( ) set )
for R being ( ( Relation-like ) ( Relation-like ) Relation) holds
( ( R : ( ( Relation-like ) ( Relation-like ) Relation) * (R : ( ( Relation-like ) ( Relation-like ) Relation) \ (id X : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) set ) ) : ( ( ) ( Relation-like ) M2( bool b2 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) )) : ( ( Relation-like ) ( Relation-like ) set ) = {} : ( ( ) ( empty Relation-like non-empty empty-yielding ) set ) implies R : ( ( Relation-like ) ( Relation-like ) Relation) * (R : ( ( Relation-like ) ( Relation-like ) Relation) \ (id (rng R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like rng b2 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -defined rng b2 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -valued ) set ) ) : ( ( ) ( Relation-like ) M2( bool b2 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) )) : ( ( Relation-like ) ( Relation-like ) set ) = {} : ( ( ) ( empty Relation-like non-empty empty-yielding ) set ) ) & ( (R : ( ( Relation-like ) ( Relation-like ) Relation) \ (id X : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) set ) ) : ( ( ) ( Relation-like ) M2( bool b2 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) )) * R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( Relation-like ) ( Relation-like ) set ) = {} : ( ( ) ( empty Relation-like non-empty empty-yielding ) set ) implies (R : ( ( Relation-like ) ( Relation-like ) Relation) \ (id (dom R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like dom b2 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -defined dom b2 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -valued ) set ) ) : ( ( ) ( Relation-like ) M2( bool b2 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) )) * R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( Relation-like ) ( Relation-like ) set ) = {} : ( ( ) ( empty Relation-like non-empty empty-yielding ) set ) ) ) ;

definition
let R be ( ( Relation-like ) ( Relation-like ) Relation) ;
func CL R -> ( ( Relation-like ) ( Relation-like ) Relation) equals :: SYSREL:def 1
R : ( ( Relation-like ) ( Relation-like ) set ) /\ (id (dom R : ( ( Relation-like ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like dom R : ( ( Relation-like ) ( Relation-like ) set ) : ( ( ) ( ) set ) -defined dom R : ( ( Relation-like ) ( Relation-like ) set ) : ( ( ) ( ) set ) -valued ) set ) : ( ( ) ( Relation-like ) set ) ;
end;

theorem :: SYSREL:25
for x, y being ( ( ) ( ) set )
for R being ( ( Relation-like ) ( Relation-like ) Relation) st [x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) ] : ( ( ) ( ) set ) in CL R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( Relation-like ) ( Relation-like ) Relation) holds
( x : ( ( ) ( ) set ) in dom (CL R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) & x : ( ( ) ( ) set ) = y : ( ( ) ( ) set ) ) ;

theorem :: SYSREL:26
for R being ( ( Relation-like ) ( Relation-like ) Relation) holds dom (CL R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) = rng (CL R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) ;

theorem :: SYSREL:27
for x being ( ( ) ( ) set )
for R being ( ( Relation-like ) ( Relation-like ) Relation) holds
( ( x : ( ( ) ( ) set ) in dom (CL R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) implies ( x : ( ( ) ( ) set ) in dom R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) & [x : ( ( ) ( ) set ) ,x : ( ( ) ( ) set ) ] : ( ( ) ( ) set ) in R : ( ( Relation-like ) ( Relation-like ) Relation) ) ) & ( x : ( ( ) ( ) set ) in dom R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) & [x : ( ( ) ( ) set ) ,x : ( ( ) ( ) set ) ] : ( ( ) ( ) set ) in R : ( ( Relation-like ) ( Relation-like ) Relation) implies x : ( ( ) ( ) set ) in dom (CL R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) ) & ( x : ( ( ) ( ) set ) in rng (CL R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) implies ( x : ( ( ) ( ) set ) in dom R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) & [x : ( ( ) ( ) set ) ,x : ( ( ) ( ) set ) ] : ( ( ) ( ) set ) in R : ( ( Relation-like ) ( Relation-like ) Relation) ) ) & ( x : ( ( ) ( ) set ) in dom R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) & [x : ( ( ) ( ) set ) ,x : ( ( ) ( ) set ) ] : ( ( ) ( ) set ) in R : ( ( Relation-like ) ( Relation-like ) Relation) implies x : ( ( ) ( ) set ) in rng (CL R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) ) & ( x : ( ( ) ( ) set ) in rng (CL R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) implies ( x : ( ( ) ( ) set ) in rng R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) & [x : ( ( ) ( ) set ) ,x : ( ( ) ( ) set ) ] : ( ( ) ( ) set ) in R : ( ( Relation-like ) ( Relation-like ) Relation) ) ) & ( x : ( ( ) ( ) set ) in rng R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) & [x : ( ( ) ( ) set ) ,x : ( ( ) ( ) set ) ] : ( ( ) ( ) set ) in R : ( ( Relation-like ) ( Relation-like ) Relation) implies x : ( ( ) ( ) set ) in rng (CL R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) ) & ( x : ( ( ) ( ) set ) in dom (CL R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) implies ( x : ( ( ) ( ) set ) in rng R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) & [x : ( ( ) ( ) set ) ,x : ( ( ) ( ) set ) ] : ( ( ) ( ) set ) in R : ( ( Relation-like ) ( Relation-like ) Relation) ) ) & ( x : ( ( ) ( ) set ) in rng R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) & [x : ( ( ) ( ) set ) ,x : ( ( ) ( ) set ) ] : ( ( ) ( ) set ) in R : ( ( Relation-like ) ( Relation-like ) Relation) implies x : ( ( ) ( ) set ) in dom (CL R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) ) ) ;

theorem :: SYSREL:28
for R being ( ( Relation-like ) ( Relation-like ) Relation) holds CL R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( Relation-like ) ( Relation-like ) Relation) = id (dom (CL R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like dom (CL b1 : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -defined dom (CL b1 : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -valued ) set ) ;

theorem :: SYSREL:29
for x, y being ( ( ) ( ) set )
for R being ( ( Relation-like ) ( Relation-like ) Relation) holds
( ( R : ( ( Relation-like ) ( Relation-like ) Relation) * R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( Relation-like ) ( Relation-like ) set ) = R : ( ( Relation-like ) ( Relation-like ) Relation) & R : ( ( Relation-like ) ( Relation-like ) Relation) * (R : ( ( Relation-like ) ( Relation-like ) Relation) \ (CL R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( Relation-like ) M2( bool b3 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) )) : ( ( Relation-like ) ( Relation-like ) set ) = {} : ( ( ) ( empty Relation-like non-empty empty-yielding ) set ) & [x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) ] : ( ( ) ( ) set ) in R : ( ( Relation-like ) ( Relation-like ) Relation) & x : ( ( ) ( ) set ) <> y : ( ( ) ( ) set ) implies ( x : ( ( ) ( ) set ) in (dom R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) \ (dom (CL R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) : ( ( ) ( ) M2( bool (dom b3 : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) & y : ( ( ) ( ) set ) in dom (CL R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) ) ) & ( R : ( ( Relation-like ) ( Relation-like ) Relation) * R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( Relation-like ) ( Relation-like ) set ) = R : ( ( Relation-like ) ( Relation-like ) Relation) & (R : ( ( Relation-like ) ( Relation-like ) Relation) \ (CL R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( Relation-like ) M2( bool b3 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) )) * R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( Relation-like ) ( Relation-like ) set ) = {} : ( ( ) ( empty Relation-like non-empty empty-yielding ) set ) & [x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) ] : ( ( ) ( ) set ) in R : ( ( Relation-like ) ( Relation-like ) Relation) & x : ( ( ) ( ) set ) <> y : ( ( ) ( ) set ) implies ( y : ( ( ) ( ) set ) in (rng R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) \ (dom (CL R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) : ( ( ) ( ) M2( bool (rng b3 : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) & x : ( ( ) ( ) set ) in dom (CL R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) ) ) ) ;

theorem :: SYSREL:30
for x, y being ( ( ) ( ) set )
for R being ( ( Relation-like ) ( Relation-like ) Relation) holds
( ( R : ( ( Relation-like ) ( Relation-like ) Relation) * R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( Relation-like ) ( Relation-like ) set ) = R : ( ( Relation-like ) ( Relation-like ) Relation) & R : ( ( Relation-like ) ( Relation-like ) Relation) * (R : ( ( Relation-like ) ( Relation-like ) Relation) \ (id (dom R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like dom b3 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -defined dom b3 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -valued ) set ) ) : ( ( ) ( Relation-like ) M2( bool b3 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) )) : ( ( Relation-like ) ( Relation-like ) set ) = {} : ( ( ) ( empty Relation-like non-empty empty-yielding ) set ) & [x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) ] : ( ( ) ( ) set ) in R : ( ( Relation-like ) ( Relation-like ) Relation) & x : ( ( ) ( ) set ) <> y : ( ( ) ( ) set ) implies ( x : ( ( ) ( ) set ) in (dom R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) \ (dom (CL R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) : ( ( ) ( ) M2( bool (dom b3 : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) & y : ( ( ) ( ) set ) in dom (CL R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) ) ) & ( R : ( ( Relation-like ) ( Relation-like ) Relation) * R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( Relation-like ) ( Relation-like ) set ) = R : ( ( Relation-like ) ( Relation-like ) Relation) & (R : ( ( Relation-like ) ( Relation-like ) Relation) \ (id (dom R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like dom b3 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -defined dom b3 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -valued ) set ) ) : ( ( ) ( Relation-like ) M2( bool b3 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) )) * R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( Relation-like ) ( Relation-like ) set ) = {} : ( ( ) ( empty Relation-like non-empty empty-yielding ) set ) & [x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) ] : ( ( ) ( ) set ) in R : ( ( Relation-like ) ( Relation-like ) Relation) & x : ( ( ) ( ) set ) <> y : ( ( ) ( ) set ) implies ( y : ( ( ) ( ) set ) in (rng R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) \ (dom (CL R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) : ( ( ) ( ) M2( bool (rng b3 : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) )) & x : ( ( ) ( ) set ) in dom (CL R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) ) ) ) ;

theorem :: SYSREL:31
for R being ( ( Relation-like ) ( Relation-like ) Relation) holds
( ( R : ( ( Relation-like ) ( Relation-like ) Relation) * R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( Relation-like ) ( Relation-like ) set ) = R : ( ( Relation-like ) ( Relation-like ) Relation) & R : ( ( Relation-like ) ( Relation-like ) Relation) * (R : ( ( Relation-like ) ( Relation-like ) Relation) \ (id (dom R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like dom b1 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -defined dom b1 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -valued ) set ) ) : ( ( ) ( Relation-like ) M2( bool b1 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) )) : ( ( Relation-like ) ( Relation-like ) set ) = {} : ( ( ) ( empty Relation-like non-empty empty-yielding ) set ) implies ( dom (CL R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) = rng R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) & rng (CL R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) = rng R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) ) ) & ( R : ( ( Relation-like ) ( Relation-like ) Relation) * R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( Relation-like ) ( Relation-like ) set ) = R : ( ( Relation-like ) ( Relation-like ) Relation) & (R : ( ( Relation-like ) ( Relation-like ) Relation) \ (id (dom R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like dom b1 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -defined dom b1 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -valued ) set ) ) : ( ( ) ( Relation-like ) M2( bool b1 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) )) * R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( Relation-like ) ( Relation-like ) set ) = {} : ( ( ) ( empty Relation-like non-empty empty-yielding ) set ) implies ( dom (CL R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) = dom R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) & rng (CL R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) = dom R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) ) ) ) ;

theorem :: SYSREL:32
for R being ( ( Relation-like ) ( Relation-like ) Relation) holds
( dom (CL R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) c= dom R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) & rng (CL R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) c= rng R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) & rng (CL R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) c= dom R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) & dom (CL R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) c= rng R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) ) ;

theorem :: SYSREL:33
for R being ( ( Relation-like ) ( Relation-like ) Relation) holds
( id (dom (CL R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like dom (CL b1 : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -defined dom (CL b1 : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -valued ) set ) c= id (dom R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like dom b1 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -defined dom b1 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -valued ) set ) & id (rng (CL R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like rng (CL b1 : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -defined rng (CL b1 : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -valued ) set ) c= id (dom R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like dom b1 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -defined dom b1 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -valued ) set ) ) ;

theorem :: SYSREL:34
for R being ( ( Relation-like ) ( Relation-like ) Relation) holds
( id (dom (CL R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like dom (CL b1 : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -defined dom (CL b1 : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -valued ) set ) c= R : ( ( Relation-like ) ( Relation-like ) Relation) & id (rng (CL R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like rng (CL b1 : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -defined rng (CL b1 : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -valued ) set ) c= R : ( ( Relation-like ) ( Relation-like ) Relation) ) ;

theorem :: SYSREL:35
for X being ( ( ) ( ) set )
for R being ( ( Relation-like ) ( Relation-like ) Relation) holds
( ( id X : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) set ) c= R : ( ( Relation-like ) ( Relation-like ) Relation) & (id X : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) set ) * (R : ( ( Relation-like ) ( Relation-like ) Relation) \ (id X : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) set ) ) : ( ( ) ( Relation-like ) M2( bool b2 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) )) : ( ( Relation-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined ) set ) = {} : ( ( ) ( empty Relation-like non-empty empty-yielding ) set ) implies R : ( ( Relation-like ) ( Relation-like ) Relation) | X : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like ) set ) = id X : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) set ) ) & ( id X : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) set ) c= R : ( ( Relation-like ) ( Relation-like ) Relation) & (R : ( ( Relation-like ) ( Relation-like ) Relation) \ (id X : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) set ) ) : ( ( ) ( Relation-like ) M2( bool b2 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) )) * (id X : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) set ) : ( ( Relation-like ) ( Relation-like b1 : ( ( ) ( ) set ) -valued ) set ) = {} : ( ( ) ( empty Relation-like non-empty empty-yielding ) set ) implies X : ( ( ) ( ) set ) |` R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( Relation-like ) ( Relation-like ) set ) = id X : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued ) set ) ) ) ;

theorem :: SYSREL:36
for R being ( ( Relation-like ) ( Relation-like ) Relation) holds
( ( (id (dom (CL R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like dom (CL b1 : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -defined dom (CL b1 : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -valued ) set ) * (R : ( ( Relation-like ) ( Relation-like ) Relation) \ (id (dom (CL R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like dom (CL b1 : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -defined dom (CL b1 : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -valued ) set ) ) : ( ( ) ( Relation-like ) M2( bool b1 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) )) : ( ( Relation-like ) ( Relation-like dom (CL b1 : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -defined ) set ) = {} : ( ( ) ( empty Relation-like non-empty empty-yielding ) set ) implies ( R : ( ( Relation-like ) ( Relation-like ) Relation) | (dom (CL R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like ) set ) = id (dom (CL R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like dom (CL b1 : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -defined dom (CL b1 : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -valued ) set ) & R : ( ( Relation-like ) ( Relation-like ) Relation) | (rng (CL R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like ) set ) = id (dom (CL R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like dom (CL b1 : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -defined dom (CL b1 : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -valued ) set ) ) ) & ( (R : ( ( Relation-like ) ( Relation-like ) Relation) \ (id (rng (CL R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like rng (CL b1 : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -defined rng (CL b1 : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -valued ) set ) ) : ( ( ) ( Relation-like ) M2( bool b1 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) )) * (id (rng (CL R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like rng (CL b1 : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -defined rng (CL b1 : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -valued ) set ) : ( ( Relation-like ) ( Relation-like rng (CL b1 : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -valued ) set ) = {} : ( ( ) ( empty Relation-like non-empty empty-yielding ) set ) implies ( (dom (CL R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) |` R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( Relation-like ) ( Relation-like ) set ) = id (dom (CL R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like dom (CL b1 : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -defined dom (CL b1 : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -valued ) set ) & (rng (CL R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) |` R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( Relation-like ) ( Relation-like ) set ) = id (rng (CL R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like rng (CL b1 : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -defined rng (CL b1 : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -valued ) set ) ) ) ) ;

theorem :: SYSREL:37
for R being ( ( Relation-like ) ( Relation-like ) Relation) holds
( ( R : ( ( Relation-like ) ( Relation-like ) Relation) * (R : ( ( Relation-like ) ( Relation-like ) Relation) \ (id (dom R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like dom b1 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -defined dom b1 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -valued ) set ) ) : ( ( ) ( Relation-like ) M2( bool b1 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) )) : ( ( Relation-like ) ( Relation-like ) set ) = {} : ( ( ) ( empty Relation-like non-empty empty-yielding ) set ) implies (id (dom (CL R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like dom (CL b1 : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -defined dom (CL b1 : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -valued ) set ) * (R : ( ( Relation-like ) ( Relation-like ) Relation) \ (id (dom (CL R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like dom (CL b1 : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -defined dom (CL b1 : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -valued ) set ) ) : ( ( ) ( Relation-like ) M2( bool b1 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) )) : ( ( Relation-like ) ( Relation-like dom (CL b1 : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -defined ) set ) = {} : ( ( ) ( empty Relation-like non-empty empty-yielding ) set ) ) & ( (R : ( ( Relation-like ) ( Relation-like ) Relation) \ (id (dom R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like dom b1 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -defined dom b1 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -valued ) set ) ) : ( ( ) ( Relation-like ) M2( bool b1 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) )) * R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( Relation-like ) ( Relation-like ) set ) = {} : ( ( ) ( empty Relation-like non-empty empty-yielding ) set ) implies (R : ( ( Relation-like ) ( Relation-like ) Relation) \ (id (dom (CL R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like dom (CL b1 : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -defined dom (CL b1 : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -valued ) set ) ) : ( ( ) ( Relation-like ) M2( bool b1 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) )) * (id (dom (CL R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like dom (CL b1 : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -defined dom (CL b1 : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -valued ) set ) : ( ( Relation-like ) ( Relation-like dom (CL b1 : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -valued ) set ) = {} : ( ( ) ( empty Relation-like non-empty empty-yielding ) set ) ) ) ;

theorem :: SYSREL:38
for S, R being ( ( Relation-like ) ( Relation-like ) Relation) holds
( ( S : ( ( Relation-like ) ( Relation-like ) Relation) * R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( Relation-like ) ( Relation-like ) set ) = S : ( ( Relation-like ) ( Relation-like ) Relation) & R : ( ( Relation-like ) ( Relation-like ) Relation) * (R : ( ( Relation-like ) ( Relation-like ) Relation) \ (id (dom R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like dom b2 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -defined dom b2 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -valued ) set ) ) : ( ( ) ( Relation-like ) M2( bool b2 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) )) : ( ( Relation-like ) ( Relation-like ) set ) = {} : ( ( ) ( empty Relation-like non-empty empty-yielding ) set ) implies S : ( ( Relation-like ) ( Relation-like ) Relation) * (R : ( ( Relation-like ) ( Relation-like ) Relation) \ (id (dom R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like dom b2 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -defined dom b2 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -valued ) set ) ) : ( ( ) ( Relation-like ) M2( bool b2 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) )) : ( ( Relation-like ) ( Relation-like ) set ) = {} : ( ( ) ( empty Relation-like non-empty empty-yielding ) set ) ) & ( R : ( ( Relation-like ) ( Relation-like ) Relation) * S : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( Relation-like ) ( Relation-like ) set ) = S : ( ( Relation-like ) ( Relation-like ) Relation) & (R : ( ( Relation-like ) ( Relation-like ) Relation) \ (id (dom R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like dom b2 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -defined dom b2 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -valued ) set ) ) : ( ( ) ( Relation-like ) M2( bool b2 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) )) * R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( Relation-like ) ( Relation-like ) set ) = {} : ( ( ) ( empty Relation-like non-empty empty-yielding ) set ) implies (R : ( ( Relation-like ) ( Relation-like ) Relation) \ (id (dom R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like dom b2 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -defined dom b2 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -valued ) set ) ) : ( ( ) ( Relation-like ) M2( bool b2 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) )) * S : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( Relation-like ) ( Relation-like ) set ) = {} : ( ( ) ( empty Relation-like non-empty empty-yielding ) set ) ) ) ;

theorem :: SYSREL:39
for S, R being ( ( Relation-like ) ( Relation-like ) Relation) holds
( ( S : ( ( Relation-like ) ( Relation-like ) Relation) * R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( Relation-like ) ( Relation-like ) set ) = S : ( ( Relation-like ) ( Relation-like ) Relation) & R : ( ( Relation-like ) ( Relation-like ) Relation) * (R : ( ( Relation-like ) ( Relation-like ) Relation) \ (id (dom R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like dom b2 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -defined dom b2 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -valued ) set ) ) : ( ( ) ( Relation-like ) M2( bool b2 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) )) : ( ( Relation-like ) ( Relation-like ) set ) = {} : ( ( ) ( empty Relation-like non-empty empty-yielding ) set ) implies CL S : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( Relation-like ) ( Relation-like ) Relation) c= CL R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( Relation-like ) ( Relation-like ) Relation) ) & ( R : ( ( Relation-like ) ( Relation-like ) Relation) * S : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( Relation-like ) ( Relation-like ) set ) = S : ( ( Relation-like ) ( Relation-like ) Relation) & (R : ( ( Relation-like ) ( Relation-like ) Relation) \ (id (dom R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like dom b2 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -defined dom b2 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -valued ) set ) ) : ( ( ) ( Relation-like ) M2( bool b2 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) )) * R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( Relation-like ) ( Relation-like ) set ) = {} : ( ( ) ( empty Relation-like non-empty empty-yielding ) set ) implies CL S : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( Relation-like ) ( Relation-like ) Relation) c= CL R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( Relation-like ) ( Relation-like ) Relation) ) ) ;

theorem :: SYSREL:40
for S, R being ( ( Relation-like ) ( Relation-like ) Relation) holds
( ( S : ( ( Relation-like ) ( Relation-like ) Relation) * R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( Relation-like ) ( Relation-like ) set ) = S : ( ( Relation-like ) ( Relation-like ) Relation) & R : ( ( Relation-like ) ( Relation-like ) Relation) * (R : ( ( Relation-like ) ( Relation-like ) Relation) \ (id (dom R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like dom b2 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -defined dom b2 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -valued ) set ) ) : ( ( ) ( Relation-like ) M2( bool b2 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) )) : ( ( Relation-like ) ( Relation-like ) set ) = {} : ( ( ) ( empty Relation-like non-empty empty-yielding ) set ) & R : ( ( Relation-like ) ( Relation-like ) Relation) * S : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( Relation-like ) ( Relation-like ) set ) = R : ( ( Relation-like ) ( Relation-like ) Relation) & S : ( ( Relation-like ) ( Relation-like ) Relation) * (S : ( ( Relation-like ) ( Relation-like ) Relation) \ (id (dom S : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like dom b1 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -defined dom b1 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -valued ) set ) ) : ( ( ) ( Relation-like ) M2( bool b1 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) )) : ( ( Relation-like ) ( Relation-like ) set ) = {} : ( ( ) ( empty Relation-like non-empty empty-yielding ) set ) implies CL S : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( Relation-like ) ( Relation-like ) Relation) = CL R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( Relation-like ) ( Relation-like ) Relation) ) & ( R : ( ( Relation-like ) ( Relation-like ) Relation) * S : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( Relation-like ) ( Relation-like ) set ) = S : ( ( Relation-like ) ( Relation-like ) Relation) & (R : ( ( Relation-like ) ( Relation-like ) Relation) \ (id (dom R : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like dom b2 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -defined dom b2 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -valued ) set ) ) : ( ( ) ( Relation-like ) M2( bool b2 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) )) * R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( Relation-like ) ( Relation-like ) set ) = {} : ( ( ) ( empty Relation-like non-empty empty-yielding ) set ) & S : ( ( Relation-like ) ( Relation-like ) Relation) * R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( Relation-like ) ( Relation-like ) set ) = R : ( ( Relation-like ) ( Relation-like ) Relation) & (S : ( ( Relation-like ) ( Relation-like ) Relation) \ (id (dom S : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like dom b1 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -defined dom b1 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -valued ) set ) ) : ( ( ) ( Relation-like ) M2( bool b1 : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) )) * S : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( Relation-like ) ( Relation-like ) set ) = {} : ( ( ) ( empty Relation-like non-empty empty-yielding ) set ) implies CL S : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( Relation-like ) ( Relation-like ) Relation) = CL R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( Relation-like ) ( Relation-like ) Relation) ) ) ;