let y be object ; :: according to ZFMISC_1:def 10 :: thesis: for y being object st y in {x} & y in {x} holds
y = y
let z be object ; :: thesis: ( y in {x} & z in {x} implies y = z )
assume that
A1: y in {x} and
A2: z in {x} ; :: thesis: y = z
y = x by A1, TARSKI:def 1;
hence y = z by A2, TARSKI:def 1; :: thesis: verum