let Y be set ; :: thesis: Y |` {} = {}
for x, y being set holds not [x,y] in Y |` {} by Def12;
hence Y |` {} = {} by Th37; :: thesis: verum