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