environ
vocabularies HIDDEN, XBOOLE_0, TARSKI, ZFMISC_1, SUBSET_1, RELAT_1, VALUED_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1;
definitions TARSKI, XBOOLE_0, ZFMISC_1;
theorems TARSKI, XBOOLE_0, ZFMISC_1, ENUMSET1, XBOOLE_1, XTUPLE_0;
schemes XBOOLE_0;
registrations XBOOLE_0, ZFMISC_1, XTUPLE_0;
constructors HIDDEN, TARSKI, SUBSET_1, ZFMISC_1, XTUPLE_0, XBOOLE_0;
requirements HIDDEN, SUBSET, BOOLE;
equalities TARSKI, XBOOLE_0;
expansions TARSKI, XBOOLE_0;
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 )