theorem :: MARGREL1:9

for D being non empty set holds empty_rel D = {}