theorem :: RELAT_1:155

for X being set
for R being Relation st not R | X is empty-yielding holds
not R is empty-yielding ;