:: RELSET_1 semantic presentation

begin


definition
let X, Y be set ;
mode Relation of X,Y is Subset of [:X,Y:];
end;

registration
let X, Y be set ;
cluster  ->  Relation-like for Element of bool [:X,Y:];
coherence
 for b1 being Subset of [:X,Y:] holds b1 is Relation-like ;
end;

registration
let X, Y be set ;
cluster  -> X -defined Y -valued for Element of bool [:X,Y:];
coherence
 for b1 being Relation of X,Y holds
( b1 is X -defined & b1 is Y -valued )
proof
let R be Relation of X,Y; ::_thesis: ( R is X -defined & R is Y -valued )
thus  dom R c= X :: according to RELAT_1:def_18 ::_thesis: R is Y -valued
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom R or x in X )
assume  x in dom R ; ::_thesis: x in X
then  ex y being set st [x,y] in R by XTUPLE_0:def_12;
hence  x in X by ZFMISC_1:87; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3,RELAT_1:def_19 ::_thesis: ( not y in rng R or y in Y )
assume  y in rng R ; ::_thesis: y in Y
then  ex x being set st [x,y] in R by XTUPLE_0:def_13;
hence  y in Y by ZFMISC_1:87; ::_thesis: verum
end;
end;


definition
let X, Y be set ;
let R be Relation of X,Y;
let Z be set ;
:: original: c=
redefine predR c= Z means :: RELSET_1:def 1
 for x being Element of X
for y being Element of Y st [x,y] in R holds
[x,y] in Z;
compatibility
 ( R c= Z iff for x being Element of X
for y being Element of Y st [x,y] in R holds
[x,y] in Z )
proof
thus  ( R c= Z implies for x being Element of X
for y being Element of Y st [x,y] in R holds
[x,y] in Z ) ; ::_thesis: ( ( for x being Element of X
for y being Element of Y st [x,y] in R holds
[x,y] in Z ) implies R c= Z )
assume A1: for x being Element of X
for y being Element of Y st [x,y] in R holds
[x,y] in Z ; ::_thesis: R c= Z
let a, b be set ; :: according to RELAT_1:def_3 ::_thesis: ( not [a,b] in R or [a,b] in Z )
assume A2: [a,b] in R ; ::_thesis: [a,b] in Z
then reconsider a9 = a as Element of X by ZFMISC_1:87;
reconsider b9 = b as Element of Y by A2, ZFMISC_1:87;
 [a9,b9] in Z by A1, A2;
hence  [a,b] in Z ; ::_thesis: verum
end;
end;

:: deftheorem  defines c= RELSET_1:def_1_:_
 for X, Y being set
for R being Relation of X,Y
for Z being set holds
( R c= Z iff for x being Element of X
for y being Element of Y st [x,y] in R holds
[x,y] in Z );

definition
let X, Y be set ;
let P, R be Relation of X,Y;
:: original: =
redefine predP = R means :: RELSET_1:def 2
 for x being Element of X
for y being Element of Y holds
( [x,y] in P iff [x,y] in R );
compatibility
 ( P = R iff for x being Element of X
for y being Element of Y holds
( [x,y] in P iff [x,y] in R ) )
proof
thus  ( P = R implies for x being Element of X
for y being Element of Y holds
( [x,y] in P iff [x,y] in R ) ) ; ::_thesis: ( ( for x being Element of X
for y being Element of Y holds
( [x,y] in P iff [x,y] in R ) ) implies P = R )
assume A1: for x being Element of X
for y being Element of Y holds
( [x,y] in P iff [x,y] in R ) ; ::_thesis: P = R
let a, b be set ; :: according to RELAT_1:def_2 ::_thesis: ( ( not [a,b] in P or [a,b] in R ) & ( not [a,b] in R or [a,b] in P ) )
hereby  ::_thesis: ( not [a,b] in R or [a,b] in P )
assume A2: [a,b] in P ; ::_thesis: [a,b] in R
then reconsider a9 = a as Element of X by ZFMISC_1:87;
reconsider b9 = b as Element of Y by A2, ZFMISC_1:87;
 [a9,b9] in R by A1, A2;
hence  [a,b] in R ; ::_thesis: verum
end;
assume A3: [a,b] in R ; ::_thesis: [a,b] in P
then reconsider a9 = a as Element of X by ZFMISC_1:87;
reconsider b9 = b as Element of Y by A3, ZFMISC_1:87;
 [a9,b9] in P by A1, A3;
hence  [a,b] in P ; ::_thesis: verum
end;
end;

:: deftheorem  defines = RELSET_1:def_2_:_
 for X, Y being set
for P, R being Relation of X,Y holds
( P = R iff for x being Element of X
for y being Element of Y holds
( [x,y] in P iff [x,y] in R ) );

theorem :: RELSET_1:1
for A, X, Y being set
for R being Relation of X,Y st A c= R holds
A is Relation of X,Y by XBOOLE_1:1;

theorem :: RELSET_1:2
for a, X, Y being set
for R being Relation of X,Y st a in R holds
ex x, y being set st
( a = [x,y] & x in X & y in Y )
proof
let a, X, Y be set ; ::_thesis: for R being Relation of X,Y st a in R holds
ex x, y being set st
( a = [x,y] & x in X & y in Y )
let R be Relation of X,Y; ::_thesis: ( a in R implies ex x, y being set st
( a = [x,y] & x in X & y in Y ) )
assume A1: a in R ; ::_thesis: ex x, y being set st
( a = [x,y] & x in X & y in Y )
then consider x, y being set  such that
A2: a = [x,y] by RELAT_1:def_1;
 ( x in X & y in Y ) by A1, A2, ZFMISC_1:87;
hence  ex x, y being set st
( a = [x,y] & x in X & y in Y ) by A2; ::_thesis: verum
end;

theorem :: RELSET_1:3
for x, X, y, Y being set st x in X & y in Y holds
{[x,y]} is Relation of X,Y
proof
let x, X, y, Y be set ; ::_thesis: ( x in X & y in Y implies {[x,y]} is Relation of X,Y )
assume  ( x in X & y in Y ) ; ::_thesis: {[x,y]} is Relation of X,Y
then  [x,y] in [:X,Y:] by ZFMISC_1:87;
hence  {[x,y]} is Relation of X,Y by ZFMISC_1:31; ::_thesis: verum
end;

theorem :: RELSET_1:4
for X, Y being set
for R being Relation st dom R c= X & rng R c= Y holds
R is Relation of X,Y
proof
let X, Y be set ; ::_thesis: for R being Relation st dom R c= X & rng R c= Y holds
R is Relation of X,Y
let R be Relation; ::_thesis: ( dom R c= X & rng R c= Y implies R is Relation of X,Y )
assume  ( dom R c= X & rng R c= Y ) ; ::_thesis: R is Relation of X,Y
then  ( R c= [:(dom R),(rng R):] & [:(dom R),(rng R):] c= [:X,Y:] ) by RELAT_1:7, ZFMISC_1:96;
hence  R is Relation of X,Y by XBOOLE_1:1; ::_thesis: verum
end;

theorem :: RELSET_1:5
for X, X1, Y being set
for R being Relation of X,Y st dom R c= X1 holds
R is Relation of X1,Y
proof
let X, X1, Y be set ; ::_thesis: for R being Relation of X,Y st dom R c= X1 holds
R is Relation of X1,Y
let R be Relation of X,Y; ::_thesis: ( dom R c= X1 implies R is Relation of X1,Y )
A1: rng R c= Y by RELAT_1:def_19;
assume  dom R c= X1 ; ::_thesis: R is Relation of X1,Y
then  ( R c= [:(dom R),(rng R):] & [:(dom R),(rng R):] c= [:X1,Y:] ) by A1, RELAT_1:7, ZFMISC_1:96;
hence  R is Relation of X1,Y by XBOOLE_1:1; ::_thesis: verum
end;

theorem :: RELSET_1:6
for Y, Y1, X being set
for R being Relation of X,Y st rng R c= Y1 holds
R is Relation of X,Y1
proof
let Y, Y1, X be set ; ::_thesis: for R being Relation of X,Y st rng R c= Y1 holds
R is Relation of X,Y1
let R be Relation of X,Y; ::_thesis: ( rng R c= Y1 implies R is Relation of X,Y1 )
A1: dom R c= X by RELAT_1:def_18;
assume  rng R c= Y1 ; ::_thesis: R is Relation of X,Y1
then  ( R c= [:(dom R),(rng R):] & [:(dom R),(rng R):] c= [:X,Y1:] ) by A1, RELAT_1:7, ZFMISC_1:96;
hence  R is Relation of X,Y1 by XBOOLE_1:1; ::_thesis: verum
end;

theorem :: RELSET_1:7
for X, X1, Y, Y1 being set
for R being Relation of X,Y st X c= X1 & Y c= Y1 holds
R is Relation of X1,Y1
proof
let X, X1, Y, Y1 be set ; ::_thesis: for R being Relation of X,Y st X c= X1 & Y c= Y1 holds
R is Relation of X1,Y1
let R be Relation of X,Y; ::_thesis: ( X c= X1 & Y c= Y1 implies R is Relation of X1,Y1 )
assume  ( X c= X1 & Y c= Y1 ) ; ::_thesis: R is Relation of X1,Y1
then  [:X,Y:] c= [:X1,Y1:] by ZFMISC_1:96;
hence  R is Relation of X1,Y1 by XBOOLE_1:1; ::_thesis: verum
end;

registration
let X be set ;
let R, S be X -defined Relation;
clusterR \/ S -> X -defined ;
coherence
 R \/ S is X -defined
proof
A1: dom (R \/ S) = (dom R) \/ (dom S) by RELAT_1:1;
 ( dom R c= X & dom S c= X ) by RELAT_1:def_18;
hence  dom (R \/ S) c= X by A1, XBOOLE_1:8; :: according to RELAT_1:def_18 ::_thesis: verum
end;
end;

registration
let X be set ;
let R be X -defined Relation;
let S be Relation;
clusterR /\ S -> X -defined ;
coherence
 R /\ S is X -defined
proof
 R /\ S c= R by XBOOLE_1:17;
then  ( dom R c= X & dom (R /\ S) c= dom R ) by RELAT_1:11, RELAT_1:def_18;
hence  dom (R /\ S) c= X by XBOOLE_1:1; :: according to RELAT_1:def_18 ::_thesis: verum
end;
clusterR \ S -> X -defined ;
coherence
 R \ S is X -defined ;
end;

registration
let X be set ;
let R, S be X -valued Relation;
clusterR \/ S -> X -valued ;
coherence
 R \/ S is X -valued
proof
A1: rng (R \/ S) = (rng R) \/ (rng S) by RELAT_1:12;
 ( rng R c= X & rng S c= X ) by RELAT_1:def_19;
hence  rng (R \/ S) c= X by A1, XBOOLE_1:8; :: according to RELAT_1:def_19 ::_thesis: verum
end;
end;

registration
let X be set ;
let R be X -valued Relation;
let S be Relation;
clusterR /\ S -> X -valued ;
coherence
 R /\ S is X -valued
proof
 R /\ S c= R by XBOOLE_1:17;
then  ( rng R c= X & rng (R /\ S) c= rng R ) by RELAT_1:11, RELAT_1:def_19;
hence  rng (R /\ S) c= X by XBOOLE_1:1; :: according to RELAT_1:def_19 ::_thesis: verum
end;
clusterR \ S -> X -valued ;
coherence
 R \ S is X -valued ;
end;

definition
let X be set ;
let R be X -defined Relation;
:: original: dom
redefine func dom R ->  Subset of X;
coherence
 dom R is Subset of X by RELAT_1:def_18;
end;

definition
let X be set ;
let R be X -valued Relation;
:: original: rng
redefine func rng R ->  Subset of X;
coherence
 rng R is Subset of X by RELAT_1:def_19;
end;

theorem :: RELSET_1:8
for X, Y being set
for R being Relation of X,Y holds field R c= X \/ Y
proof
let X, Y be set ; ::_thesis: for R being Relation of X,Y holds field R c= X \/ Y
let R be Relation of X,Y; ::_thesis: field R c= X \/ Y
 (dom R) \/ (rng R) c= X \/ Y by XBOOLE_1:13;
hence  field R c= X \/ Y ; ::_thesis: verum
end;

theorem :: RELSET_1:9
for Y, X being set
for R being Relation of X,Y holds
( ( for x being set st x in X holds
ex y being set st [x,y] in R ) iff dom R = X )
proof
let Y, X be set ; ::_thesis: for R being Relation of X,Y holds
( ( for x being set st x in X holds
ex y being set st [x,y] in R ) iff dom R = X )
let R be Relation of X,Y; ::_thesis: ( ( for x being set st x in X holds
ex y being set st [x,y] in R ) iff dom R = X )
thus  ( ( for x being set st x in X holds
ex y being set st [x,y] in R ) implies dom R = X ) ::_thesis: ( dom R = X implies for x being set st x in X holds
ex y being set st [x,y] in R )
proof
assume A1: for x being set st x in X holds
ex y being set st [x,y] in R ; ::_thesis: dom R = X
now__::_thesis:_for_x_being_set_holds_
(_x_in_dom_R_iff_x_in_X_)
let x be set ; ::_thesis: ( x in dom R iff x in X )
now__::_thesis:_(_x_in_X_implies_x_in_dom_R_)
assume  x in X ; ::_thesis: x in dom R
then  ex y being set st [x,y] in R by A1;
hence  x in dom R by XTUPLE_0:def_12; ::_thesis: verum
end;
hence  ( x in dom R iff x in X ) ; ::_thesis: verum
end;
hence  dom R = X by TARSKI:1; ::_thesis: verum
end;
thus  ( dom R = X implies for x being set st x in X holds
ex y being set st [x,y] in R ) by XTUPLE_0:def_12; ::_thesis: verum
end;

theorem :: RELSET_1:10
for X, Y being set
for R being Relation of X,Y holds
( ( for y being set st y in Y holds
ex x being set st [x,y] in R ) iff rng R = Y )
proof
let X, Y be set ; ::_thesis: for R being Relation of X,Y holds
( ( for y being set st y in Y holds
ex x being set st [x,y] in R ) iff rng R = Y )
let R be Relation of X,Y; ::_thesis: ( ( for y being set st y in Y holds
ex x being set st [x,y] in R ) iff rng R = Y )
thus  ( ( for y being set st y in Y holds
ex x being set st [x,y] in R ) implies rng R = Y ) ::_thesis: ( rng R = Y implies for y being set st y in Y holds
ex x being set st [x,y] in R )
proof
assume A1: for y being set st y in Y holds
ex x being set st [x,y] in R ; ::_thesis: rng R = Y
now__::_thesis:_for_y_being_set_holds_
(_y_in_rng_R_iff_y_in_Y_)
let y be set ; ::_thesis: ( y in rng R iff y in Y )
now__::_thesis:_(_y_in_Y_implies_y_in_rng_R_)
assume  y in Y ; ::_thesis: y in rng R
then  ex x being set st [x,y] in R by A1;
hence  y in rng R by XTUPLE_0:def_13; ::_thesis: verum
end;
hence  ( y in rng R iff y in Y ) ; ::_thesis: verum
end;
hence  rng R = Y by TARSKI:1; ::_thesis: verum
end;
thus  ( rng R = Y implies for y being set st y in Y holds
ex x being set st [x,y] in R ) by XTUPLE_0:def_13; ::_thesis: verum
end;

definition
let X, Y be set ;
let R be Relation of X,Y;
:: original: ~
redefine funcR ~  ->  Relation of Y,X;
coherence
 R ~ is Relation of Y,X
proof
now__::_thesis:_for_x,_y_being_set_st_[x,y]_in_R_~_holds_
[x,y]_in_[:Y,X:]
let x, y be set ; ::_thesis: ( [x,y] in R ~ implies [x,y] in [:Y,X:] )
assume  [x,y] in R ~ ; ::_thesis: [x,y] in [:Y,X:]
then  [y,x] in R by RELAT_1:def_7;
hence  [x,y] in [:Y,X:] by ZFMISC_1:88; ::_thesis: verum
end;
hence  R ~ is Relation of Y,X by RELAT_1:def_3; ::_thesis: verum
end;
end;

definition
let X, Y1, Y2, Z be set ;
let P be Relation of X,Y1;
let R be Relation of Y2,Z;
:: original: *
redefine funcP * R ->  Relation of X,Z;
coherence
 P * R is Relation of X,Z
proof
now__::_thesis:_for_x,_z_being_set_st_[x,z]_in_P_*_R_holds_
[x,z]_in_[:X,Z:]
let x, z be set ; ::_thesis: ( [x,z] in P * R implies [x,z] in [:X,Z:] )
assume  [x,z] in P * R ; ::_thesis: [x,z] in [:X,Z:]
then  ex y being set st
( [x,y] in P & [y,z] in R ) by RELAT_1:def_8;
then  ( x in X & z in Z ) by ZFMISC_1:87;
hence  [x,z] in [:X,Z:] by ZFMISC_1:87; ::_thesis: verum
end;
hence  P * R is Relation of X,Z by RELAT_1:def_3; ::_thesis: verum
end;
end;

theorem :: RELSET_1:11
for X, Y being set
for R being Relation of X,Y holds
( dom (R ~) = rng R & rng (R ~) = dom R )
proof
let X, Y be set ; ::_thesis: for R being Relation of X,Y holds
( dom (R ~) = rng R & rng (R ~) = dom R )
let R be Relation of X,Y; ::_thesis: ( dom (R ~) = rng R & rng (R ~) = dom R )
now__::_thesis:_for_x_being_set_holds_
(_x_in_dom_(R_~)_iff_x_in_rng_R_)
let x be set ; ::_thesis: ( x in dom (R ~) iff x in rng R )
A1: now__::_thesis:_(_x_in_rng_R_implies_x_in_dom_(R_~)_)
assume  x in rng R ; ::_thesis: x in dom (R ~)
then consider y being set  such that
A2: [y,x] in R by XTUPLE_0:def_13;
 [x,y] in R ~ by A2, RELAT_1:def_7;
hence  x in dom (R ~) by XTUPLE_0:def_12; ::_thesis: verum
end;
now__::_thesis:_(_x_in_dom_(R_~)_implies_x_in_rng_R_)
assume  x in dom (R ~) ; ::_thesis: x in rng R
then consider y being set  such that
A3: [x,y] in R ~ by XTUPLE_0:def_12;
 [y,x] in R by A3, RELAT_1:def_7;
hence  x in rng R by XTUPLE_0:def_13; ::_thesis: verum
end;
hence  ( x in dom (R ~) iff x in rng R ) by A1; ::_thesis: verum
end;
hence  dom (R ~) = rng R by TARSKI:1; ::_thesis: rng (R ~) = dom R
now__::_thesis:_for_x_being_set_holds_
(_x_in_rng_(R_~)_iff_x_in_dom_R_)
let x be set ; ::_thesis: ( x in rng (R ~) iff x in dom R )
A4: now__::_thesis:_(_x_in_dom_R_implies_x_in_rng_(R_~)_)
assume  x in dom R ; ::_thesis: x in rng (R ~)
then consider y being set  such that
A5: [x,y] in R by XTUPLE_0:def_12;
 [y,x] in R ~ by A5, RELAT_1:def_7;
hence  x in rng (R ~) by XTUPLE_0:def_13; ::_thesis: verum
end;
now__::_thesis:_(_x_in_rng_(R_~)_implies_x_in_dom_R_)
assume  x in rng (R ~) ; ::_thesis: x in dom R
then consider y being set  such that
A6: [y,x] in R ~ by XTUPLE_0:def_13;
 [x,y] in R by A6, RELAT_1:def_7;
hence  x in dom R by XTUPLE_0:def_12; ::_thesis: verum
end;
hence  ( x in rng (R ~) iff x in dom R ) by A4; ::_thesis: verum
end;
hence  rng (R ~) = dom R by TARSKI:1; ::_thesis: verum
end;

theorem :: RELSET_1:12
for X, Y being set holds {} is Relation of X,Y by XBOOLE_1:2;

registration
let A be empty set ;
let B be set ;
cluster  ->  empty for Element of bool [:A,B:];
coherence
 for b1 being Relation of A,B holds b1 is empty ;
cluster  ->  empty for Element of bool [:B,A:];
coherence
 for b1 being Relation of B,A holds b1 is empty ;
end;

theorem Th13: :: RELSET_1:13
for X being set holds id X c= [:X,X:]
proof
let X be set ; ::_thesis: id X c= [:X,X:]
 [:X,X:] c= [:X,X:] ;
then reconsider R = [:X,X:] as Relation of X,X ;
 for x, y being set st [x,y] in id X holds
[x,y] in R
proof
let x, y be set ; ::_thesis: ( [x,y] in id X implies [x,y] in R )
assume  [x,y] in id X ; ::_thesis: [x,y] in R
then  ( x in X & x = y ) by RELAT_1:def_10;
hence  [x,y] in R by ZFMISC_1:87; ::_thesis: verum
end;
hence  id X c= [:X,X:] by RELAT_1:def_3; ::_thesis: verum
end;

theorem :: RELSET_1:14
for X being set holds id X is Relation of X,X by Th13;

theorem Th15: :: RELSET_1:15
for X, Y, A being set
for R being Relation of X,Y st id A c= R holds
( A c= dom R & A c= rng R )
proof
let X, Y, A be set ; ::_thesis: for R being Relation of X,Y st id A c= R holds
( A c= dom R & A c= rng R )
let R be Relation of X,Y; ::_thesis: ( id A c= R implies ( A c= dom R & A c= rng R ) )
assume A1: id A c= R ; ::_thesis: ( A c= dom R & A c= rng R )
thus  A c= dom R ::_thesis: A c= rng R
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in dom R )
assume  x in A ; ::_thesis: x in dom R
then  [x,x] in id A by RELAT_1:def_10;
hence  x in dom R by A1, XTUPLE_0:def_12; ::_thesis: verum
end;
thus  A c= rng R ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in rng R )
assume  x in A ; ::_thesis: x in rng R
then  [x,x] in id A by RELAT_1:def_10;
hence  x in rng R by A1, XTUPLE_0:def_13; ::_thesis: verum
end;
end;

theorem :: RELSET_1:16
for Y, X being set
for R being Relation of X,Y st id X c= R holds
( X = dom R & X c= rng R )
proof
let Y, X be set ; ::_thesis: for R being Relation of X,Y st id X c= R holds
( X = dom R & X c= rng R )
let R be Relation of X,Y; ::_thesis: ( id X c= R implies ( X = dom R & X c= rng R ) )
assume A1: id X c= R ; ::_thesis: ( X = dom R & X c= rng R )
then  X c= dom R by Th15;
hence  X = dom R by XBOOLE_0:def_10; ::_thesis: X c= rng R
thus  X c= rng R by A1, Th15; ::_thesis: verum
end;

theorem :: RELSET_1:17
for X, Y being set
for R being Relation of X,Y st id Y c= R holds
( Y c= dom R & Y = rng R )
proof
let X, Y be set ; ::_thesis: for R being Relation of X,Y st id Y c= R holds
( Y c= dom R & Y = rng R )
let R be Relation of X,Y; ::_thesis: ( id Y c= R implies ( Y c= dom R & Y = rng R ) )
assume A1: id Y c= R ; ::_thesis: ( Y c= dom R & Y = rng R )
hence  Y c= dom R by Th15; ::_thesis: Y = rng R
 Y c= rng R by A1, Th15;
hence  Y = rng R by XBOOLE_0:def_10; ::_thesis: verum
end;

definition
let X, Y be set ;
let R be Relation of X,Y;
let A be set ;
:: original: |
redefine funcR | A ->  Relation of X,Y;
coherence
 R | A is Relation of X,Y
proof
now__::_thesis:_for_x,_y_being_set_st_[x,y]_in_R_|_A_holds_
[x,y]_in_[:X,Y:]
let x, y be set ; ::_thesis: ( [x,y] in R | A implies [x,y] in [:X,Y:] )
assume  [x,y] in R | A ; ::_thesis: [x,y] in [:X,Y:]
then  [x,y] in R by RELAT_1:def_11;
hence  [x,y] in [:X,Y:] ; ::_thesis: verum
end;
hence  R | A is Relation of X,Y by RELAT_1:def_3; ::_thesis: verum
end;
end;

definition
let X, Y, B be set ;
let R be Relation of X,Y;
:: original: |`
redefine funcB |` R ->  Relation of X,Y;
coherence
 B |` R is Relation of X,Y
proof
now__::_thesis:_for_x,_y_being_set_st_[x,y]_in_B_|`_R_holds_
[x,y]_in_[:X,Y:]
let x, y be set ; ::_thesis: ( [x,y] in B |` R implies [x,y] in [:X,Y:] )
assume  [x,y] in B |` R ; ::_thesis: [x,y] in [:X,Y:]
then  [x,y] in R by RELAT_1:def_12;
hence  [x,y] in [:X,Y:] ; ::_thesis: verum
end;
hence  B |` R is Relation of X,Y by RELAT_1:def_3; ::_thesis: verum
end;
end;

theorem :: RELSET_1:18
for X, X1, Y being set
for R being Relation of X,Y holds R | X1 is Relation of X1,Y
proof
let X, X1, Y be set ; ::_thesis: for R being Relation of X,Y holds R | X1 is Relation of X1,Y
let R be Relation of X,Y; ::_thesis: R | X1 is Relation of X1,Y
now__::_thesis:_for_x,_y_being_set_st_[x,y]_in_R_|_X1_holds_
[x,y]_in_[:X1,Y:]
let x, y be set ; ::_thesis: ( [x,y] in R | X1 implies [x,y] in [:X1,Y:] )
assume  [x,y] in R | X1 ; ::_thesis: [x,y] in [:X1,Y:]
then  ( x in X1 & y in Y ) by RELAT_1:def_11, ZFMISC_1:87;
hence  [x,y] in [:X1,Y:] by ZFMISC_1:87; ::_thesis: verum
end;
hence  R | X1 is Relation of X1,Y by RELAT_1:def_3; ::_thesis: verum
end;

theorem :: RELSET_1:19
for Y, X, X1 being set
for R being Relation of X,Y st X c= X1 holds
R | X1 = R
proof
let Y, X, X1 be set ; ::_thesis: for R being Relation of X,Y st X c= X1 holds
R | X1 = R
let R be Relation of X,Y; ::_thesis: ( X c= X1 implies R | X1 = R )
assume A1: X c= X1 ; ::_thesis: R | X1 = R
now__::_thesis:_for_x,_y_being_set_holds_
(_[x,y]_in_R_|_X1_iff_[x,y]_in_R_)
let x, y be set ; ::_thesis: ( [x,y] in R | X1 iff [x,y] in R )
now__::_thesis:_(_[x,y]_in_R_implies_[x,y]_in_R_|_X1_)
assume A2: [x,y] in R ; ::_thesis: [x,y] in R | X1
then  x in X by ZFMISC_1:87;
hence  [x,y] in R | X1 by A1, A2, RELAT_1:def_11; ::_thesis: verum
end;
hence  ( [x,y] in R | X1 iff [x,y] in R ) by RELAT_1:def_11; ::_thesis: verum
end;
hence  R | X1 = R by RELAT_1:def_2; ::_thesis: verum
end;

theorem :: RELSET_1:20
for Y, Y1, X being set
for R being Relation of X,Y holds Y1 |` R is Relation of X,Y1
proof
let Y, Y1, X be set ; ::_thesis: for R being Relation of X,Y holds Y1 |` R is Relation of X,Y1
let R be Relation of X,Y; ::_thesis: Y1 |` R is Relation of X,Y1
now__::_thesis:_for_x,_y_being_set_st_[x,y]_in_Y1_|`_R_holds_
[x,y]_in_[:X,Y1:]
let x, y be set ; ::_thesis: ( [x,y] in Y1 |` R implies [x,y] in [:X,Y1:] )
assume  [x,y] in Y1 |` R ; ::_thesis: [x,y] in [:X,Y1:]
then  ( y in Y1 & x in X ) by RELAT_1:def_12, ZFMISC_1:87;
hence  [x,y] in [:X,Y1:] by ZFMISC_1:87; ::_thesis: verum
end;
hence  Y1 |` R is Relation of X,Y1 by RELAT_1:def_3; ::_thesis: verum
end;

theorem :: RELSET_1:21
for X, Y, Y1 being set
for R being Relation of X,Y st Y c= Y1 holds
Y1 |` R = R
proof
let X, Y, Y1 be set ; ::_thesis: for R being Relation of X,Y st Y c= Y1 holds
Y1 |` R = R
let R be Relation of X,Y; ::_thesis: ( Y c= Y1 implies Y1 |` R = R )
assume A1: Y c= Y1 ; ::_thesis: Y1 |` R = R
now__::_thesis:_for_x,_y_being_set_holds_
(_[x,y]_in_Y1_|`_R_iff_[x,y]_in_R_)
let x, y be set ; ::_thesis: ( [x,y] in Y1 |` R iff [x,y] in R )
now__::_thesis:_(_[x,y]_in_R_implies_[x,y]_in_Y1_|`_R_)
assume A2: [x,y] in R ; ::_thesis: [x,y] in Y1 |` R
then  y in Y by ZFMISC_1:87;
hence  [x,y] in Y1 |` R by A1, A2, RELAT_1:def_12; ::_thesis: verum
end;
hence  ( [x,y] in Y1 |` R iff [x,y] in R ) by RELAT_1:def_12; ::_thesis: verum
end;
hence  Y1 |` R = R by RELAT_1:def_2; ::_thesis: verum
end;

definition
let X, Y be set ;
let R be Relation of X,Y;
let A be set ;
:: original: .:
redefine funcR .: A ->  Subset of Y;
coherence
 R .: A is Subset of Y
proof
 R .: A c= rng R by RELAT_1:111;
hence  R .: A is Subset of Y by XBOOLE_1:1; ::_thesis: verum
end;
:: original: "
redefine funcR " A ->  Subset of X;
coherence
 R " A is Subset of X
proof
 R " A c= dom R by RELAT_1:132;
hence  R " A is Subset of X by XBOOLE_1:1; ::_thesis: verum
end;
end;

theorem Th22: :: RELSET_1:22
for X, Y being set
for R being Relation of X,Y holds
( R .: X = rng R & R " Y = dom R )
proof
let X, Y be set ; ::_thesis: for R being Relation of X,Y holds
( R .: X = rng R & R " Y = dom R )
let R be Relation of X,Y; ::_thesis: ( R .: X = rng R & R " Y = dom R )
now__::_thesis:_for_y_being_set_holds_
(_y_in_R_.:_X_iff_y_in_rng_R_)
let y be set ; ::_thesis: ( y in R .: X iff y in rng R )
A1: now__::_thesis:_(_y_in_rng_R_implies_y_in_R_.:_X_)
assume  y in rng R ; ::_thesis: y in R .: X
then consider x being set  such that
A2: [x,y] in R by XTUPLE_0:def_13;
 x in X by A2, ZFMISC_1:87;
hence  y in R .: X by A2, RELAT_1:def_13; ::_thesis: verum
end;
now__::_thesis:_(_y_in_R_.:_X_implies_y_in_rng_R_)
assume  y in R .: X ; ::_thesis: y in rng R
then  ex x being set st
( [x,y] in R & x in X ) by RELAT_1:def_13;
hence  y in rng R by XTUPLE_0:def_13; ::_thesis: verum
end;
hence  ( y in R .: X iff y in rng R ) by A1; ::_thesis: verum
end;
hence  R .: X = rng R by TARSKI:1; ::_thesis: R " Y = dom R
now__::_thesis:_for_x_being_set_holds_
(_x_in_R_"_Y_iff_x_in_dom_R_)
let x be set ; ::_thesis: ( x in R " Y iff x in dom R )
A3: now__::_thesis:_(_x_in_dom_R_implies_x_in_R_"_Y_)
assume  x in dom R ; ::_thesis: x in R " Y
then consider y being set  such that
A4: [x,y] in R by XTUPLE_0:def_12;
 y in Y by A4, ZFMISC_1:87;
hence  x in R " Y by A4, RELAT_1:def_14; ::_thesis: verum
end;
now__::_thesis:_(_x_in_R_"_Y_implies_x_in_dom_R_)
assume  x in R " Y ; ::_thesis: x in dom R
then  ex y being set st
( [x,y] in R & y in Y ) by RELAT_1:def_14;
hence  x in dom R by XTUPLE_0:def_12; ::_thesis: verum
end;
hence  ( x in R " Y iff x in dom R ) by A3; ::_thesis: verum
end;
hence  R " Y = dom R by TARSKI:1; ::_thesis: verum
end;

theorem :: RELSET_1:23
for Y, X being set
for R being Relation of X,Y holds
( R .: (R " Y) = rng R & R " (R .: X) = dom R )
proof
let Y, X be set ; ::_thesis: for R being Relation of X,Y holds
( R .: (R " Y) = rng R & R " (R .: X) = dom R )
let R be Relation of X,Y; ::_thesis: ( R .: (R " Y) = rng R & R " (R .: X) = dom R )
 ( R " Y = dom R & R .: X = rng R ) by Th22;
hence  ( R .: (R " Y) = rng R & R " (R .: X) = dom R ) by RELAT_1:113, RELAT_1:134; ::_thesis: verum
end;

scheme :: RELSET_1:sch 1
RelOnSetEx{ F1() ->  set , F2() ->  set , P1[ set , set ] } :
 ex R being Relation of F1(),F2() st
for x, y being set holds
( [x,y] in R iff ( x in F1() & y in F2() & P1[x,y] ) )
proof
consider R being Relation such that
A1: for x, y being set holds
( [x,y] in R iff ( x in F1() & y in F2() & P1[x,y] ) ) from RELAT_1:sch_1();
 R c= [:F1(),F2():]
proof
let x1, x2 be set ; :: according to RELAT_1:def_3 ::_thesis: ( not [x1,x2] in R or [x1,x2] in [:F1(),F2():] )
assume  [x1,x2] in R ; ::_thesis: [x1,x2] in [:F1(),F2():]
then  ( x1 in F1() & x2 in F2() ) by A1;
hence  [x1,x2] in [:F1(),F2():] by ZFMISC_1:87; ::_thesis: verum
end;
then reconsider R = R as Relation of F1(),F2() ;
take  R ; ::_thesis: for x, y being set holds
( [x,y] in R iff ( x in F1() & y in F2() & P1[x,y] ) )
thus  for x, y being set holds
( [x,y] in R iff ( x in F1() & y in F2() & P1[x,y] ) ) by A1; ::_thesis: verum
end;

definition
let X be set ;
mode Relation of X is Relation of X,X;
end;


registration
let D be non empty set ;
cluster id D ->  non empty ;
coherence
 not id D is empty
proof
now__::_thesis:_not_id_D_=_{}
set y = the Element of D;
A1: [ the Element of D, the Element of D] in id D by RELAT_1:def_10;
assume  id D = {} ; ::_thesis: contradiction
hence  contradiction by A1; ::_thesis: verum
end;
hence  not id D is empty ; ::_thesis: verum
end;
end;

theorem :: RELSET_1:24
for D, E being non empty set
for R being Relation of D,E
for x being Element of D holds
( x in dom R iff ex y being Element of E st [x,y] in R )
proof
let D, E be non empty set ; ::_thesis: for R being Relation of D,E
for x being Element of D holds
( x in dom R iff ex y being Element of E st [x,y] in R )
let R be Relation of D,E; ::_thesis: for x being Element of D holds
( x in dom R iff ex y being Element of E st [x,y] in R )
let x be Element of D; ::_thesis: ( x in dom R iff ex y being Element of E st [x,y] in R )
thus  ( x in dom R implies ex y being Element of E st [x,y] in R ) ::_thesis: ( ex y being Element of E st [x,y] in R implies x in dom R )
proof
assume  x in dom R ; ::_thesis: ex y being Element of E st [x,y] in R
then consider y being set  such that
A1: [x,y] in R by XTUPLE_0:def_12;
reconsider b = y as Element of E by A1, ZFMISC_1:87;
take  b ; ::_thesis: [x,b] in R
thus  [x,b] in R by A1; ::_thesis: verum
end;
given y being Element of E such that A2: [x,y] in R ; ::_thesis: x in dom R
thus  x in dom R by A2, XTUPLE_0:def_12; ::_thesis: verum
end;

theorem :: RELSET_1:25
for E, D being non empty set
for R being Relation of D,E
for y being set holds
( y in rng R iff ex x being Element of D st [x,y] in R )
proof
let E, D be non empty set ; ::_thesis: for R being Relation of D,E
for y being set holds
( y in rng R iff ex x being Element of D st [x,y] in R )
let R be Relation of D,E; ::_thesis: for y being set holds
( y in rng R iff ex x being Element of D st [x,y] in R )
let y be set ; ::_thesis: ( y in rng R iff ex x being Element of D st [x,y] in R )
thus  ( y in rng R implies ex x being Element of D st [x,y] in R ) ::_thesis: ( ex x being Element of D st [x,y] in R implies y in rng R )
proof
assume  y in rng R ; ::_thesis: ex x being Element of D st [x,y] in R
then consider x being set  such that
A1: [x,y] in R by XTUPLE_0:def_13;
reconsider a = x as Element of D by A1, ZFMISC_1:87;
take  a ; ::_thesis: [a,y] in R
thus  [a,y] in R by A1; ::_thesis: verum
end;
given x being Element of D such that A2: [x,y] in R ; ::_thesis: y in rng R
thus  y in rng R by A2, XTUPLE_0:def_13; ::_thesis: verum
end;

theorem :: RELSET_1:26
for D, E being non empty set
for R being Relation of D,E st dom R <> {} holds
ex y being Element of E st y in rng R
proof
let D, E be non empty set ; ::_thesis: for R being Relation of D,E st dom R <> {} holds
ex y being Element of E st y in rng R
let R be Relation of D,E; ::_thesis: ( dom R <> {} implies ex y being Element of E st y in rng R )
assume  dom R <> {} ; ::_thesis: ex y being Element of E st y in rng R
then  rng R <> {} by RELAT_1:42;
then  ex y being set st y in rng R by XBOOLE_0:def_1;
hence  ex y being Element of E st y in rng R ; ::_thesis: verum
end;

theorem :: RELSET_1:27
for E, D being non empty set
for R being Relation of D,E st rng R <> {} holds
ex x being Element of D st x in dom R
proof
let E, D be non empty set ; ::_thesis: for R being Relation of D,E st rng R <> {} holds
ex x being Element of D st x in dom R
let R be Relation of D,E; ::_thesis: ( rng R <> {} implies ex x being Element of D st x in dom R )
assume  rng R <> {} ; ::_thesis: ex x being Element of D st x in dom R
then  dom R <> {} by RELAT_1:42;
then  ex x being set st x in dom R by XBOOLE_0:def_1;
hence  ex x being Element of D st x in dom R ; ::_thesis: verum
end;

theorem :: RELSET_1:28
for D, E, F being non empty set
for P being Relation of D,E
for R being Relation of E,F
for x, z being set holds
( [x,z] in P * R iff ex y being Element of E st
( [x,y] in P & [y,z] in R ) )
proof
let D, E, F be non empty set ; ::_thesis: for P being Relation of D,E
for R being Relation of E,F
for x, z being set holds
( [x,z] in P * R iff ex y being Element of E st
( [x,y] in P & [y,z] in R ) )
let P be Relation of D,E; ::_thesis: for R being Relation of E,F
for x, z being set holds
( [x,z] in P * R iff ex y being Element of E st
( [x,y] in P & [y,z] in R ) )
let R be Relation of E,F; ::_thesis: for x, z being set holds
( [x,z] in P * R iff ex y being Element of E st
( [x,y] in P & [y,z] in R ) )
let x, z be set ; ::_thesis: ( [x,z] in P * R iff ex y being Element of E st
( [x,y] in P & [y,z] in R ) )
thus  ( [x,z] in P * R implies ex y being Element of E st
( [x,y] in P & [y,z] in R ) ) ::_thesis: ( ex y being Element of E st
( [x,y] in P & [y,z] in R ) implies [x,z] in P * R )
proof
assume  [x,z] in P * R ; ::_thesis: ex y being Element of E st
( [x,y] in P & [y,z] in R )
then consider y being set  such that
A1: [x,y] in P and
A2: [y,z] in R by RELAT_1:def_8;
reconsider a = y as Element of E by A1, ZFMISC_1:87;
take  a ; ::_thesis: ( [x,a] in P & [a,z] in R )
thus  ( [x,a] in P & [a,z] in R ) by A1, A2; ::_thesis: verum
end;
given y being Element of E such that A3: ( [x,y] in P & [y,z] in R ) ; ::_thesis: [x,z] in P * R
thus  [x,z] in P * R by A3, RELAT_1:def_8; ::_thesis: verum
end;

theorem :: RELSET_1:29
for E, D1, D being non empty set
for R being Relation of D,E
for y being Element of E holds
( y in R .: D1 iff ex x being Element of D st
( [x,y] in R & x in D1 ) )
proof
let E, D1, D be non empty set ; ::_thesis: for R being Relation of D,E
for y being Element of E holds
( y in R .: D1 iff ex x being Element of D st
( [x,y] in R & x in D1 ) )
let R be Relation of D,E; ::_thesis: for y being Element of E holds
( y in R .: D1 iff ex x being Element of D st
( [x,y] in R & x in D1 ) )
let y be Element of E; ::_thesis: ( y in R .: D1 iff ex x being Element of D st
( [x,y] in R & x in D1 ) )
thus  ( y in R .: D1 implies ex x being Element of D st
( [x,y] in R & x in D1 ) ) ::_thesis: ( ex x being Element of D st
( [x,y] in R & x in D1 ) implies y in R .: D1 )
proof
assume  y in R .: D1 ; ::_thesis: ex x being Element of D st
( [x,y] in R & x in D1 )
then consider x being set  such that
A1: [x,y] in R and
A2: x in D1 by RELAT_1:def_13;
reconsider a = x as Element of D by A1, ZFMISC_1:87;
take  a ; ::_thesis: ( [a,y] in R & a in D1 )
thus  ( [a,y] in R & a in D1 ) by A1, A2; ::_thesis: verum
end;
given x being Element of D such that A3: ( [x,y] in R & x in D1 ) ; ::_thesis: y in R .: D1
thus  y in R .: D1 by A3, RELAT_1:def_13; ::_thesis: verum
end;

theorem :: RELSET_1:30
for D, D2, E being non empty set
for R being Relation of D,E
for x being Element of D holds
( x in R " D2 iff ex y being Element of E st
( [x,y] in R & y in D2 ) )
proof
let D, D2, E be non empty set ; ::_thesis: for R being Relation of D,E
for x being Element of D holds
( x in R " D2 iff ex y being Element of E st
( [x,y] in R & y in D2 ) )
let R be Relation of D,E; ::_thesis: for x being Element of D holds
( x in R " D2 iff ex y being Element of E st
( [x,y] in R & y in D2 ) )
let x be Element of D; ::_thesis: ( x in R " D2 iff ex y being Element of E st
( [x,y] in R & y in D2 ) )
thus  ( x in R " D2 implies ex y being Element of E st
( [x,y] in R & y in D2 ) ) ::_thesis: ( ex y being Element of E st
( [x,y] in R & y in D2 ) implies x in R " D2 )
proof
assume  x in R " D2 ; ::_thesis: ex y being Element of E st
( [x,y] in R & y in D2 )
then consider y being set  such that
A1: [x,y] in R and
A2: y in D2 by RELAT_1:def_14;
reconsider b = y as Element of E by A1, ZFMISC_1:87;
take  b ; ::_thesis: ( [x,b] in R & b in D2 )
thus  ( [x,b] in R & b in D2 ) by A1, A2; ::_thesis: verum
end;
given y being Element of E such that A3: ( [x,y] in R & y in D2 ) ; ::_thesis: x in R " D2
thus  x in R " D2 by A3, RELAT_1:def_14; ::_thesis: verum
end;

scheme :: RELSET_1:sch 2
RelOnDomEx{ F1() ->  non empty set , F2() ->  non empty set , P1[ set , set ] } :
 ex R being Relation of F1(),F2() st
for x being Element of F1()
for y being Element of F2() holds
( [x,y] in R iff P1[x,y] )
proof
consider R being Relation of F1(),F2() such that
A1: for x, y being set holds
( [x,y] in R iff ( x in F1() & y in F2() & P1[x,y] ) ) from RELSET_1:sch_1();
take  R ; ::_thesis: for x being Element of F1()
for y being Element of F2() holds
( [x,y] in R iff P1[x,y] )
thus  for x being Element of F1()
for y being Element of F2() holds
( [x,y] in R iff P1[x,y] ) by A1; ::_thesis: verum
end;

begin

scheme :: RELSET_1:sch 3
Sch3{ F1() ->  set , F2() ->  Subset of F1(), F3( set ) ->  set } :
 ex R being Relation of F2() st
for i being Element of F1() st i in F2() holds
Im (R,i) = F3(i)
provided
A1: for i being Element of F1() st i in F2() holds
F3(i) c= F2()
proof
defpred S1[ set , set ] means $2 in F3($1);
consider R being Relation of F2() such that
A2: for x, y being set holds
( [x,y] in R iff ( x in F2() & y in F2() & S1[x,y] ) ) from RELSET_1:sch_1();
take  R ; ::_thesis: for i being Element of F1() st i in F2() holds
Im (R,i) = F3(i)
let i be Element of F1(); ::_thesis: ( i in F2() implies Im (R,i) = F3(i) )
assume A3: i in F2() ; ::_thesis: Im (R,i) = F3(i)
thus  Im (R,i) c= F3(i) :: according to XBOOLE_0:def_10 ::_thesis: F3(i) c= Im (R,i)
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in Im (R,i) or e in F3(i) )
assume  e in Im (R,i) ; ::_thesis: e in F3(i)
then consider u being set  such that
A4: [u,e] in R and
A5: u in {i} by RELAT_1:def_13;
 u = i by A5, TARSKI:def_1;
hence  e in F3(i) by A2, A4; ::_thesis: verum
end;
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in F3(i) or e in Im (R,i) )
assume A6: e in F3(i) ; ::_thesis: e in Im (R,i)
 F3(i) c= F2() by A1, A3;
then  ( i in {i} & [i,e] in R ) by A2, A3, A6, TARSKI:def_1;
hence  e in Im (R,i) by RELAT_1:def_13; ::_thesis: verum
end;

theorem :: RELSET_1:31
for N being set
for R, S being Relation of N st ( for i being set st i in N holds
Im (R,i) = Im (S,i) ) holds
R = S
proof
let N be set ; ::_thesis: for R, S being Relation of N st ( for i being set st i in N holds
Im (R,i) = Im (S,i) ) holds
R = S
let R, S be Relation of N; ::_thesis: ( ( for i being set st i in N holds
Im (R,i) = Im (S,i) ) implies R = S )
assume A1: for i being set st i in N holds
Im (R,i) = Im (S,i) ; ::_thesis: R = S
let a, b be Element of N; :: according to RELSET_1:def_2 ::_thesis: ( [a,b] in R iff [a,b] in S )
thus  ( [a,b] in R implies [a,b] in S ) ::_thesis: ( [a,b] in S implies [a,b] in R )
proof
assume A2: [a,b] in R ; ::_thesis: [a,b] in S
then A3: a in dom R by XTUPLE_0:def_12;
 a in {a} by TARSKI:def_1;
then  b in Im (R,a) by A2, RELAT_1:def_13;
then  b in Im (S,a) by A1, A3;
then  ex e being set st
( [e,b] in S & e in {a} ) by RELAT_1:def_13;
hence  [a,b] in S by TARSKI:def_1; ::_thesis: verum
end;
assume A4: [a,b] in S ; ::_thesis: [a,b] in R
then A5: a in dom S by XTUPLE_0:def_12;
 a in {a} by TARSKI:def_1;
then  b in Im (S,a) by A4, RELAT_1:def_13;
then  b in Im (R,a) by A1, A5;
then  ex e being set st
( [e,b] in R & e in {a} ) by RELAT_1:def_13;
hence  [a,b] in R by TARSKI:def_1; ::_thesis: verum
end;

scheme :: RELSET_1:sch 4
Sch4{ F1() ->  set , F2() ->  set , P1[ set , set ], F3() ->  Relation of F1(),F2(), F4() ->  Relation of F1(),F2() } :
 F3() = F4()
provided
A1: for p being Element of F1()
for q being Element of F2() holds
( [p,q] in F3() iff P1[p,q] ) and
A2: for p being Element of F1()
for q being Element of F2() holds
( [p,q] in F4() iff P1[p,q] )
proof
let y be Element of F1(); :: according to RELSET_1:def_2 ::_thesis: for y being Element of F2() holds
( [y,y] in F3() iff [y,y] in F4() )
let z be Element of F2(); ::_thesis: ( [y,z] in F3() iff [y,z] in F4() )
 ( [y,z] in F3() iff P1[y,z] ) by A1;
hence  ( [y,z] in F3() iff [y,z] in F4() ) by A2; ::_thesis: verum
end;

registration
let X, Y, Z be set ;
let f be Relation of [:X,Y:],Z;
cluster dom f ->  Relation-like ;
coherence
 dom f is Relation-like ;
end;

registration
let X, Y, Z be set ;
let f be Relation of X,[:Y,Z:];
cluster rng f ->  Relation-like ;
coherence
 rng f is Relation-like ;
end;

theorem :: RELSET_1:32
for Y, A, X being set
for P being Relation of X,Y st A misses X holds
P | A = {}
proof
let Y, A, X be set ; ::_thesis: for P being Relation of X,Y st A misses X holds
P | A = {}
let P be Relation of X,Y; ::_thesis: ( A misses X implies P | A = {} )
assume  A misses X ; ::_thesis: P | A = {}
then  A misses dom P by XBOOLE_1:63;
hence  P | A = {} by RELAT_1:152; ::_thesis: verum
end;

registration
let R be non empty Relation;
let Y be non empty Subset of (dom R);
clusterR | Y ->  non empty ;
coherence
 not R | Y is empty
proof
 dom (R | Y) = Y by RELAT_1:62;
hence  not R | Y is empty ; ::_thesis: verum
end;
end;

registration
let R be non empty Relation;
let Y be non empty Subset of (dom R);
clusterR .: Y ->  non empty ;
coherence
 not R .: Y is empty
proof
 R .: Y = rng (R | Y) by RELAT_1:115;
hence  not R .: Y is empty ; ::_thesis: verum
end;
end;

registration
let X, Y be set ;
cluster empty Relation-like X -defined Y -valued for Element of bool [:X,Y:];
existence
 ex b1 being Relation of X,Y st b1 is empty
proof
 {} is Relation of X,Y by XBOOLE_1:2;
hence  ex b1 being Relation of X,Y st b1 is empty ; ::_thesis: verum
end;
end;