begin
theorem
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 )
theorem
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 )
theorem
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 )
theorem
for
Y,
X,
X1 being
set for
R being
Relation of
X,
Y st
X c= X1 holds
R | X1 = R
begin
theorem
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
scheme
Sch4{
F1()
-> set ,
F2()
-> set ,
P1[
set ,
set ],
F3()
-> Relation of
F1(),
F2(),
F4()
-> Relation of
F1(),
F2() } :
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] )
:: RELATION AS A SUBSET OF CARTESIAN PRODUCT OF TWO SETS
:: _____________________________________________________