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