let A be non empty set ; for b being object st A <> {b} holds
ex a being Element of A st a <> b
let b be object ; ( A <> {b} implies ex a being Element of A st a <> b )
assume A1:
A <> {b}
; ex a being Element of A st a <> b
assume A2:
for a being Element of A holds a = b
; contradiction
now 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 ;
( ( a in A implies a = b ) & ( a = b implies a in A ) )thus
(
a in A implies
a = b )
by A2;
( a = b implies a in A )assume A3:
a = b
;
a in A
the
Element of
A = b
by A2;
hence
a in A
by A3;
verum end;
hence
contradiction
by A1, TARSKI:def 1; verum