set z = 4;
not 4 in {1,2,3} by ENUMSET1:def 1;
hence {1,2,3} <> {3,4} by TARSKI:def 2; :: thesis: verum