let X be set ; :: thesis: {} .: X = {}
consider y being Element of {} .: X;
assume not {} .: X = {} ; :: thesis: contradiction
then ex x being set st
( [x,y] in {} & x in X ) by Def13;
hence contradiction ; :: thesis: verum