theorem :: RELAT_1:149

for R being Relation holds
( R is empty-yielding iff for X being set st X in rng R holds
X = {} )