let X be set ; :: thesis: {X} \ X <> {}
assume {X} \ X = {} ; :: thesis: contradiction
then X in X by ZFMISC_1:60;
hence contradiction ; :: thesis: verum