theorem :: RELAT_1:81

for R being Relation holds R | {} = {} ;