theorem :: SYSREL:10

for X, Y being set
for R being Relation st X misses Y & R c= [:X,Y:] \/ [:Y,X:] holds
R | X c= [:X,Y:]