let A be non empty set ; :: thesis: for b being set st A <> {b} holds
ex a being Element of A st a <> b
let b be set ; :: thesis: ( A <> {b} implies ex a being Element of A st a <> b )
assume A1: A <> {b} ; :: thesis: ex a being Element of A st a <> b
assume A2: for a being Element of A holds a = b ; :: thesis: contradiction

now

consider a0 being Element of A;
let a be set ; :: thesis: ( ( a in A implies a = b ) & ( a = b implies a in A ) )
thus ( a in A implies a = b ) by A2; :: thesis: ( a = b implies a in A )
assume A3: a = b ; :: thesis: a in A
a0 = b by A2;
hence a in A by A3; :: thesis: verum

end;

hence contradiction by A1, TARSKI:def 1; :: thesis: verum