environ
vocabularies HIDDEN, RELAT_1, XBOOLE_0, ZFMISC_1, TARSKI, SYSREL;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1;
definitions TARSKI, XBOOLE_0, RELAT_1;
theorems ZFMISC_1, RELAT_1, TARSKI, XBOOLE_0, XBOOLE_1, XTUPLE_0;
schemes ;
registrations XBOOLE_0, RELAT_1;
constructors HIDDEN, TARSKI, SUBSET_1, RELAT_1, XTUPLE_0;
requirements HIDDEN, BOOLE, SUBSET;
equalities ;
expansions TARSKI, XBOOLE_0, RELAT_1;
Lm1:
for X, Y being set st X <> {} & Y <> {} holds
( dom [:X,Y:] = X & rng [:X,Y:] = Y )
by RELAT_1:160;
theorem
for
x,
y being
object for
X,
Y being
set for
R being
Relation holds
( (
X misses Y &
R c= [:X,Y:] \/ [:Y,X:] &
[x,y] in R &
x in X implies ( not
x in Y & not
y in X &
y in Y ) ) & (
X misses Y &
R c= [:X,Y:] \/ [:Y,X:] &
[x,y] in R &
y in Y implies ( not
y in X & not
x in Y &
x in X ) ) & (
X misses Y &
R c= [:X,Y:] \/ [:Y,X:] &
[x,y] in R &
x in Y implies ( not
x in X & not
y in Y &
y in X ) ) & (
X misses Y &
R c= [:X,Y:] \/ [:Y,X:] &
[x,y] in R &
y in X implies ( not
x in X & not
y in Y &
x in Y ) ) )
Lm2:
for X being set holds id X c= [:X,X:]