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