let Y be set ; :: thesis: {} " Y = {}
assume not {} " Y = {} ; :: thesis: contradiction
then ex y being set st
( [the Element of {} " Y,y] in {} & y in Y ) by Def14;
hence contradiction ; :: thesis: verum