let X be set ; :: thesis: {X} <> X
X in {X} by TARSKI:def 1;
hence {X} <> X ; :: thesis: verum