begin
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,
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:]