Re: (no subject)

[Piotr Rudnicki <piotr@cs.ualberta.ca>]

> 
> The unordered pair functor is commutative.  Therefore from
> 
> A: { A, B } = { C, D };
> 
>    we have both:
> 
> B: (A = C or A = D) & (B = C or B = D) by A, ZFMISC_1:10;
> C: (C = A or C = B) & (D = A or D = B) by A, ZFMISC_1:10;
> 
> and then
> 
>    A = C & B = D or A = D & B = C by B, C;
> 

I have just noticed that above, the reference to the commutativity
of the onordered pair functor is irrelevant.  Simply, two different 
instances of ZFMISC_1:10 are used to disprove the four disjuncts
of the negated proposition.

-- 
Piotr (Peter) Rudnicki