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

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