definition
let R be
Relation;
existence
ex b1 being Relation st
for x, y being object holds
( [x,y] in b1 iff [y,x] in R )
uniqueness
for b1, b2 being Relation st ( for x, y being object holds
( [x,y] in b1 iff [y,x] in R ) ) & ( for x, y being object holds
( [x,y] in b2 iff [y,x] in R ) ) holds
b1 = b2
involutiveness
for b1, b2 being Relation st ( for x, y being object holds
( [x,y] in b1 iff [y,x] in b2 ) ) holds
for x, y being object holds
( [x,y] in b2 iff [y,x] in b1 )
;
end;
definition
let P,
R be
set ;
existence
ex b1 being Relation st
for x, y being object holds
( [x,y] in b1 iff ex z being object st
( [x,z] in P & [z,y] in R ) )
uniqueness
for b1, b2 being Relation st ( for x, y being object holds
( [x,y] in b1 iff ex z being object st
( [x,z] in P & [z,y] in R ) ) ) & ( for x, y being object holds
( [x,y] in b2 iff ex z being object st
( [x,z] in P & [z,y] in R ) ) ) holds
b1 = b2
end;
definition
let R be
Relation;
let X be
set ;
existence
ex b1 being Relation st
for x, y being object holds
( [x,y] in b1 iff ( x in X & [x,y] in R ) )
uniqueness
for b1, b2 being Relation st ( for x, y being object holds
( [x,y] in b1 iff ( x in X & [x,y] in R ) ) ) & ( for x, y being object holds
( [x,y] in b2 iff ( x in X & [x,y] in R ) ) ) holds
b1 = b2
end;
definition
let Y be
set ;
let R be
Relation;
existence
ex b1 being Relation st
for x, y being object holds
( [x,y] in b1 iff ( y in Y & [x,y] in R ) )
uniqueness
for b1, b2 being Relation st ( for x, y being object holds
( [x,y] in b1 iff ( y in Y & [x,y] in R ) ) ) & ( for x, y being object holds
( [x,y] in b2 iff ( y in Y & [x,y] in R ) ) ) holds
b1 = b2
end;
Lm1:
for X, Y being set holds
( {} is X -defined & {} is Y -valued )