let x, y, z be set ; :: thesis: ( z in x & z in y & x \ {z} = y \ {z} implies x = y )
assume that
A1: z in x and
A2: z in y ; :: thesis: ( not x \ {z} = y \ {z} or x = y )
assume A3: x \ {z} = y \ {z} ; :: thesis: x = y
thus x = x \/ {z} by A1, ZFMISC_1:40
.= (y \ {z}) \/ {z} by A3, XBOOLE_1:39
.= y \/ {z} by XBOOLE_1:39
.= y by A2, ZFMISC_1:40 ; :: thesis: verum