(no subject)

[Andrzej Trybulec <trybulec@edserve.cs.shinshu-u.ac.jp>]

I wanted to justify the following step (A,B,C,D fixed):

{ A,B } = { C,D };
then A = C & B = D or A = D & B = C 

I looked to Bylinski's ZFMISC_1 (where else), I found a theorem and I
put
"by ZFMISC_1:10;" as a justification.

I called Mizar and then I observed that ZFMISC_1:10 is not what
I need. It is:
 {x1,x2} = {y1,y2} implies (x1 = y1 or x1 = y2) & (x2 = y1 or x2 = y2)
in the situation above e.g. A = C & B = C.

It was a surprize when Mizar accepted it. I appreciate comments.

Andrzej Trybulec