let A be non empty set ; :: thesis: for b being object st A <> {b} holds
ex a being Element of A st a <> b
let b be object ; :: 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 :: thesis: for a being object holds
( ( a in A implies a = b ) & ( a = b implies a in A ) )

set a0 = the Element of A;
let a be object ; :: 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
the Element of A = b by A2;
hence a in A by A3; :: thesis: verum

end;

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