theorem :: RELAT_1:107

for Y being set holds Y |` {} = {} by Def10;