:: Relations Defined on Sets
:: by Edmund Woronowicz
::
:: Received April 14, 1989
:: Copyright (c) 1990-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies RELAT_1, SUBSET_1, ZFMISC_1, TARSKI, XBOOLE_0;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1;
constructors TARSKI, SUBSET_1, RELAT_1, XTUPLE_0;
registrations XBOOLE_0, RELAT_1, SUBSET_1;
requirements SUBSET, BOOLE;
definitions TARSKI, XBOOLE_0, RELAT_1;
equalities RELAT_1;
expansions TARSKI, XBOOLE_0, RELAT_1;
theorems TARSKI, ZFMISC_1, RELAT_1, XBOOLE_0, XBOOLE_1, XTUPLE_0;
schemes RELAT_1;
begin
reserve A,B,X,X1,Y,Y1,Y2,Z for set, a,x,y,z for object;
::
:: RELATION AS A SUBSET OF CARTESIAN PRODUCT OF TWO SETS
:: _____________________________________________________
definition
let X,Y;
mode Relation of X,Y is Subset of [:X,Y:];
end;
registration
let X,Y;
cluster -> Relation-like for Subset of [:X,Y:];
coherence;
end;
registration
let X,Y;
cluster -> X-defined Y-valued for Relation of X,Y;
coherence
proof
let R be Relation of X,Y;
thus dom R c= X
proof
let x be object;
assume x in dom R;
then ex y being object st [x,y] in R by XTUPLE_0:def 12;
hence thesis by ZFMISC_1:87;
end;
let y be object;
assume y in rng R;
then ex x being object st [x,y] in R by XTUPLE_0:def 13;
hence thesis by ZFMISC_1:87;
end;
end;
reserve P,R for Relation of X,Y;
definition
let X,Y,R,Z;
redefine pred R c= Z means :: redefines c= (RELAT_1, redefinition) → c= (TARSKI, definition)
for x being Element of X, y being Element of Y
holds [x,y] in R implies [x,y] in Z;
compatibility
proof
thus R c= Z implies for x being Element of X, y being Element of Y holds [
x,y] in R implies [x,y] in Z;
assume
A1: for x being Element of X, y being Element of Y holds [x,y] in R
implies [x,y] in Z;
let a,b be object;
assume
A2: [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 Z by A1,A2;
hence thesis;
end;
end;
definition
let X,Y,P,R;
redefine pred P = R means :: redefines = (RELAT_1, redefinition) → = (XBOOLE_0, redefinition) → = (HIDDEN, definition)
for x being Element of X, y being Element of Y
holds [x,y] in P iff [x,y] in R;
compatibility
proof
thus P = R implies for x being Element of X, y being Element of Y holds [x
,y] in P iff [x,y] in R;
assume
A1: for x being Element of X, y being Element of Y holds [x,y] in P
iff [x,y] in R;
let a,b be object;
hereby
assume
A2: [a,b] in P;
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;
end;
assume
A3: [a,b] in R;
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 thesis;
end;
end;
theorem
A c= R implies A is Relation of X,Y by XBOOLE_1:1;
theorem
a in R implies ex x,y st a = [x,y] & x in X & y in Y
proof
assume
A1: a in R;
then consider x,y being object such that
A2: a = [x,y] by RELAT_1:def 1;
x in X & y in Y by A1,A2,ZFMISC_1:87;
hence thesis by A2;
end;
theorem
x in X & y in Y implies {[x,y]} is Relation of X,Y by ZFMISC_1:31,87;
theorem
for R being Relation st dom R c= X & rng R c= Y holds R is Relation of X,Y
proof
let R be Relation;
assume dom R c= X & rng R c= Y;
then R c= [:dom R, rng R:] & [:dom R, rng R:] c= [:X,Y:] by RELAT_1:7
,ZFMISC_1:96;
hence thesis by XBOOLE_1:1;
end;
theorem
dom R c= X1 implies R is Relation of X1,Y
proof
A1: rng R c= Y by RELAT_1:def 19;
assume dom R c= X1;
then R c= [:dom R, rng R:] & [:dom R, rng R:] c= [:X1,Y:] by A1,RELAT_1:7
,ZFMISC_1:96;
hence thesis by XBOOLE_1:1;
end;
theorem
rng R c= Y1 implies R is Relation of X,Y1
proof
A1: dom R c= X by RELAT_1:def 18;
assume rng R c= Y1;
then R c= [:dom R, rng R:] & [:dom R, rng R:] c= [:X,Y1:] by A1,RELAT_1:7
,ZFMISC_1:96;
hence thesis by XBOOLE_1:1;
end;
theorem
X c= X1 & Y c= Y1 implies R is Relation of X1,Y1
proof
assume X c= X1 & Y c= Y1;
then [:X,Y:] c= [:X1,Y1:] by ZFMISC_1:96;
hence thesis by XBOOLE_1:1;
end;
registration
let X;
let R,S be X-defined Relation;
cluster R \/ S -> X-defined;
coherence
proof
A1: dom(R \/ S) = dom R \/ dom S by XTUPLE_0:23;
dom R c= X & dom S c= X by RELAT_1:def 18;
hence dom(R \/ S) c= X by A1,XBOOLE_1:8;
end;
end;
registration
let X;
let R be X-defined Relation, S be Relation;
cluster R /\ S -> X-defined;
coherence
proof
R /\ S c= R by XBOOLE_1:17;
then dom R c= X & dom(R /\ S) c= dom R by RELAT_1:11,def 18;
hence dom(R /\ S) c= X;
end;
cluster R \ S -> X-defined;
coherence;
end;
registration
let X;
let R,S be X-valued Relation;
cluster R \/ S -> X-valued;
coherence
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;
end;
end;
registration
let X;
let R be X-valued Relation, S be Relation;
cluster R /\ S -> X-valued;
coherence
proof
R /\ S c= R by XBOOLE_1:17;
then rng R c= X & rng(R /\ S) c= rng R by RELAT_1:11,def 19;
hence rng(R /\ S) c= X;
end;
cluster R \ S -> X-valued;
coherence;
end;
definition let X; let R be X-defined Relation;
redefine func dom R -> Subset of X; :: redefines dom (RELAT_1, synonym) → proj1 (XTUPLE_0, definition)
coherence by RELAT_1:def 18;
end;
definition let X; let R be X-valued Relation;
redefine func rng R -> Subset of X; :: redefines rng (RELAT_1, synonym) → proj2 (XTUPLE_0, definition)
coherence by RELAT_1:def 19;
end;
theorem
field R c= X \/ Y
proof
dom R \/ rng R c= X \/ Y by XBOOLE_1:13;
hence thesis;
end;
theorem
(for x being object st x in X
ex y being object st [x,y] in R) iff dom R = X
proof
thus (for x being object st x in X ex y being object st [x,y] in R)
implies dom R = X
proof
assume
A1: for x being object st x in X ex y being object st [x,y] in R;
now
let x be object;
now
assume x in X;
then ex y being object st [x,y] in R by A1;
hence x in dom R by XTUPLE_0:def 12;
end;
hence x in dom R iff x in X;
end;
hence dom R = X by TARSKI:2;
end;
thus thesis by XTUPLE_0:def 12;
end;
theorem
(for y being object st y in Y
ex x being object st [x,y] in R) iff rng R = Y
proof
thus (for y being object st y in Y
ex x being object st [x,y] in R) implies rng R = Y
proof
assume
A1: for y being object st y in Y ex x being object st [x,y] in R;
now
let y be object;
now
assume y in Y;
then ex x being object st [x,y] in R by A1;
hence y in rng R by XTUPLE_0:def 13;
end;
hence y in rng R iff y in Y;
end;
hence rng R = Y by TARSKI:2;
end;
thus thesis by XTUPLE_0:def 13;
end;
definition
let X,Y,R;
redefine func R~ -> Relation of Y,X; :: redefines ~ (RELAT_1, definition)
coherence
proof
now
let x,y be object;
assume [x,y] in R~;
then [y,x] in R by RELAT_1:def 7;
hence [x,y] in [:Y,X:] by ZFMISC_1:88;
end;
hence thesis by RELAT_1:def 3;
end;
end;
definition
let X,Y1,Y2,Z;
let P be Relation of X,Y1;
let R be Relation of Y2,Z;
redefine func P*R -> Relation of X,Z; :: redefines * (RELAT_1, synonym) → (#) (RELAT_1, definition)
coherence
proof
now
let x,z be object;
assume [x,z] in P*R;
then ex y being object 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;
end;
hence thesis by RELAT_1:def 3;
end;
end;
theorem
dom (R~) = rng R & rng (R~) = dom R
proof
now
let x be object;
A1: now
assume x in rng R;
then consider y being object 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;
end;
now
assume x in dom (R~);
then consider y being object 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;
end;
hence x in dom (R~) iff x in rng R by A1;
end;
hence dom (R~) = rng R by TARSKI:2;
now
let x be object;
A4: now
assume x in dom R;
then consider y being object 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;
end;
now
assume x in rng (R~);
then consider y being object 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;
end;
hence x in rng (R~) iff x in dom R by A4;
end;
hence thesis by TARSKI:2;
end;
theorem
{} is Relation of X,Y by XBOOLE_1:2;
registration
let A be empty set, B be set;
cluster -> empty for Relation of A,B;
coherence;
cluster -> empty for Relation of B,A;
coherence;
end;
theorem Th13:
id X c= [:X,X:]
proof
[:X,X:] c= [:X,X:];
then reconsider R = [:X,X:] as Relation of X,X;
for x,y being object holds [x,y] in id X implies [x,y] in R
proof let x,y be object;
assume [x,y] in id X;
then x in X & x = y by RELAT_1:def 10;
hence thesis by ZFMISC_1:87;
end;
hence thesis;
end;
theorem
id X is Relation of X,X by Th13;
theorem Th15:
id A c= R implies A c= dom R & A c= rng R
proof
assume
A1: id A c= R;
thus A c= dom R
proof
let x be object;
assume x in A;
then [x,x] in id A by RELAT_1:def 10;
hence thesis by A1,XTUPLE_0:def 12;
end;
thus A c= rng R
proof
let x be object;
assume x in A;
then [x,x] in id A by RELAT_1:def 10;
hence thesis by A1,XTUPLE_0:def 13;
end;
end;
theorem
id X c= R implies X = dom R & X c= rng R
by Th15;
theorem
id Y c= R implies Y c= dom R & Y = rng R
by Th15;
definition
let X,Y,R,A;
redefine func R|A -> Relation of X,Y; :: redefines | (RELAT_1, definition)
coherence
proof
now
let x,y be object;
assume [x,y] in R|A;
then [x,y] in R by RELAT_1:def 11;
hence [x,y] in [:X,Y:];
end;
hence thesis by RELAT_1:def 3;
end;
end;
definition
let X,Y,B,R;
redefine func B|`R -> Relation of X,Y; :: redefines |` (RELAT_1, definition)
coherence
proof
now
let x,y be object;
assume [x,y] in B|`R;
then [x,y] in R by RELAT_1:def 12;
hence [x,y] in [:X,Y:];
end;
hence thesis by RELAT_1:def 3;
end;
end;
theorem
R|X1 is Relation of X1,Y
proof
now
let x,y be object;
assume [x,y] in R|X1;
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;
end;
hence thesis by RELAT_1:def 3;
end;
theorem
X c= X1 implies R|X1 = R
proof
assume
A1: X c= X1;
now
let x,y be object;
now
assume
A2: [x,y] in R;
then x in X by ZFMISC_1:87;
hence [x,y] in R|X1 by A1,A2,RELAT_1:def 11;
end;
hence [x,y] in R|X1 iff [x,y] in R by RELAT_1:def 11;
end;
hence thesis;
end;
theorem
Y1|`R is Relation of X,Y1
proof
now
let x,y be object;
assume [x,y] in Y1|`R;
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;
end;
hence thesis by RELAT_1:def 3;
end;
theorem
Y c= Y1 implies Y1|`R = R
proof
assume
A1: Y c= Y1;
now
let x,y be object;
now
assume
A2: [x,y] in R;
then y in Y by ZFMISC_1:87;
hence [x,y] in Y1|`R by A1,A2,RELAT_1:def 12;
end;
hence [x,y] in Y1|`R iff [x,y] in R by RELAT_1:def 12;
end;
hence thesis;
end;
definition
let X,Y,R,A;
redefine func R.:A -> Subset of Y; :: redefines .: (RELAT_1, definition)
coherence
proof
R.:A c= rng R by RELAT_1:111;
hence thesis by XBOOLE_1:1;
end;
redefine func R"A -> Subset of X; :: redefines " (RELAT_1, definition)
coherence
proof
R"A c= dom R by RELAT_1:132;
hence thesis by XBOOLE_1:1;
end;
end;
theorem Th22:
R.:X = rng R & R"Y = dom R
proof
now
let y be object;
A1: now
assume y in rng R;
then consider x being object 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;
end;
now
assume y in R.:X;
then ex x being object st [x,y] in R & x in X by RELAT_1:def 13;
hence y in rng R by XTUPLE_0:def 13;
end;
hence y in R.:X iff y in rng R by A1;
end;
hence R.:X = rng R by TARSKI:2;
now
let x be object;
A3: now
assume x in dom R;
then consider y being object 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;
end;
now
assume x in R"Y;
then ex y being object st [x,y] in R & y in Y by RELAT_1:def 14;
hence x in dom R by XTUPLE_0:def 12;
end;
hence x in R"Y iff x in dom R by A3;
end;
hence thesis by TARSKI:2;
end;
theorem
R.:(R"Y) = rng R & R"(R.:X) = dom R
proof
R"Y = dom R & R.:X = rng R by Th22;
hence thesis by RELAT_1:113,134;
end;
scheme
RelOnSetEx{A() -> set,B() -> set,P[object,object]}:
ex R being Relation of A(),B()
st for x,y holds [x,y] in R iff x in A() & y in B() & P[x,y] proof
consider R being Relation such that
A1: for x,y being object holds [x,y] in R iff x in A() & y in B() & P[x,y]
from
RELAT_1:sch 1;
R c= [:A(),B():]
proof
let x1,x2 be object;
assume [x1,x2] in R;
then x1 in A() & x2 in B() by A1;
hence thesis by ZFMISC_1:87;
end;
then reconsider R as Relation of A(),B();
take R;
thus thesis by A1;
end;
:: Relation on a set
definition
let X;
mode Relation of X is Relation of X,X;
end;
reserve D,D1,D2,E,F for non empty set;
reserve R for Relation of D,E;
reserve x for Element of D;
reserve y for Element of E;
registration
let D be non empty set;
cluster id D -> non empty;
coherence
proof
now
set y = the Element of D;
A1: [y,y] in id D by RELAT_1:def 10;
assume id D = {};
hence contradiction by A1;
end;
hence thesis;
end;
end;
theorem
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 x be Element of D;
thus x in dom R implies ex y being Element of E st [x,y] in R
proof
assume x in dom R;
then consider y being object 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;
thus thesis by A1;
end;
given y being Element of E such that
A2: [x,y] in R;
thus thesis by A2,XTUPLE_0:def 12;
end;
theorem
for y being object holds y in rng R iff
ex x being Element of D st [x,y] in R
proof
let y be object;
thus y in rng R implies ex x being Element of D st [x,y] in R
proof
assume y in rng R;
then consider x being object 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;
thus thesis by A1;
end;
thus thesis by XTUPLE_0:def 13;
end;
theorem
dom R <> {} implies ex y being Element of E st y in rng R
proof
assume dom R <> {};
then rng R <> {} by RELAT_1:42;
then ex y being object st y in rng R by XBOOLE_0:def 1;
hence thesis;
end;
theorem
rng R <> {} implies ex x being Element of D st x in dom R
proof
assume rng R <> {};
then dom R <> {} by RELAT_1:42;
then ex x being object st x in dom R by XBOOLE_0:def 1;
hence thesis;
end;
theorem
for P being Relation of D,E, R being Relation of E,F
for x, z being object holds [x,z] in P*R iff
ex y being Element of E st [x,y] in P & [y,z] in R
proof
let P be Relation of D,E, R be Relation of E,F;
let x, z be object;
thus [x,z] in P*R implies ex y being Element of E st [x,y] in P & [y,z] in R
proof
assume [x,z] in P*R;
then consider y being object 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;
thus thesis by A1,A2;
end;
given y such that
A3: [x,y] in P & [y,z] in R;
thus thesis by A3,RELAT_1:def 8;
end;
theorem
y in R.:D1 iff ex x being Element of D st [x,y] in R & x in D1
proof
thus y in R.:D1 implies ex x being Element of D st [x,y] in R & x in D1
proof
assume y in R.:D1;
then consider x being object 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;
thus thesis by A1,A2;
end;
given x such that
A3: [x,y] in R & x in D1;
thus thesis by A3,RELAT_1:def 13;
end;
theorem
x in R"D2 iff ex y being Element of E st [x,y] in R & y in D2
proof
thus x in R"D2 implies ex y being Element of E st [x,y] in R & y in D2
proof
assume x in R"D2;
then consider y being object 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;
thus thesis by A1,A2;
end;
given y being Element of E such that
A3: [x,y] in R & y in D2;
thus thesis by A3,RELAT_1:def 14;
end;
scheme
RelOnDomEx{A,B() -> non empty set, P[object,object]}:
ex R being Relation of A(),B
() st for x being Element of A(), y being Element of B() holds [x,y] in R iff P
[x,y] proof
consider R being Relation of A(),B() qua set such that
A1: for x,y being object holds [x,y] in R iff x in A() & y in B() & P[x,y]
from RelOnSetEx;
take R;
thus thesis by A1;
end;
begin :: Addenda
:: missing, 2006.11.04, A.T.
scheme
{ N()-> set, M() -> Subset of N(), F(object)->set }:
ex R being Relation of M()
st for i being Element of N() st i in M() holds Im(R,i) = F(i)
provided
A1: for i being Element of N() st i in M() holds F(i) c= M()
proof
defpred P[object,object] means $2 in F($1);
consider R being Relation of M() such that
A2: for x,y being object holds [x,y] in R iff x in M() & y in M() & P[x,y]
from RelOnSetEx;
take R;
let i be Element of N();
assume
A3: i in M();
thus Im(R,i) c= F(i)
proof
let e be object;
assume e in Im(R,i);
then consider u being object 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 thesis by A2,A4;
end;
let e be object;
assume
A6: e in F(i);
F(i) c= M() by A1,A3;
then i in {i} & [i,e] in R by A2,A3,A6,TARSKI:def 1;
hence thesis by RELAT_1:def 13;
end;
theorem
for N being set, 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, R,S be Relation of N such that
A1: for i being set st i in N holds Im(R,i) = Im(S,i);
let a,b be Element of N;
thus [a,b] in R implies [a,b] in S
proof
assume
A2: [a,b] in R;
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 object st [e,b] in S & e in {a} by RELAT_1:def 13;
hence thesis by TARSKI:def 1;
end;
assume
A4: [a,b] in S;
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 object st [e,b] in R & e in {a} by RELAT_1:def 13;
hence thesis by TARSKI:def 1;
end;
:: from AMI_3, 2007.06.13, A.T. (generalized)
scheme
{A,B() -> set, P[object,object], Q,R()->Relation of A(), B()}: Q() = R()
provided
A1: for p being Element of A(), q being Element of B() holds
[p,q] in Q() iff P[p,q] and
A2: for p being Element of A(), q being Element of B() holds
[p,q] in R() iff P[p,q] proof
let y be Element of A(), z be Element of B();
[y,z] in Q() iff P[y,z] by A1;
hence thesis by A2;
end;
:: missing, 2007.06.14, A.T.
registration
let X,Y,Z;
let f be Relation of [:X,Y:], Z;
cluster dom f -> Relation-like;
coherence;
end;
registration
let X,Y,Z;
let f be Relation of X, [:Y, Z:];
cluster rng f -> Relation-like;
coherence;
end;
:: missing, 2008.04.30, A.T.
theorem
A misses X implies P|A = {}
proof
assume A misses X;
then A misses dom P by XBOOLE_1:63;
hence thesis by RELAT_1:152;
end;
:: missing, 2008.09.15, A.T.
registration
let R be non empty Relation, Y be non empty Subset of dom R;
cluster R|Y -> non empty;
coherence
proof
dom(R|Y) = Y by RELAT_1:62;
hence thesis;
end;
end;
registration
let R be non empty Relation;
let Y be non empty Subset of dom R;
cluster R.:Y -> non empty;
coherence
proof
R.:Y = rng(R|Y) by RELAT_1:115;
hence thesis;
end;
end;
:: missing, 2008.11.29 A.T.
registration
let X,Y be set;
cluster empty for Relation of X,Y;
existence
proof
{} is Relation of X,Y by XBOOLE_1:2;
hence thesis;
end;
end;
scheme
{A() -> set,B() -> set,P[object,object]}:
ex R being Relation of A(),B()
st for x,y being set holds [x,y] in R iff x in A() & y in B() & P[x,y];
consider R being Relation of A(),B() such that
A1: for x,y being object holds [x,y] in R iff x in A() & y in B() & P[x,y]
from RelOnSetEx;
take R;
thus thesis by A1;
end;