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

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 ) )

hence
contradiction
by A1, TARSKI:def 1; :: thesis: verum( ( 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;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