  The derivation of Excluded Middle from AC was first given by Diaconescu (1975) in a category-theoretic setting. His proof employed essentially different ideas from the proof presented above; in particular, it makes no use of extensionality principles but instead employs the idea of the quotient of an object (or set) by an equivalence relation. It is instructive to formulate Diaconescu’s argument within IST. To do this, let us call a subset \(U\) of a set \(A\) detachable if there is a subset \(V\) of \(A\) for which \(U \cap V = \varnothing\) and \(U \cup V = A\).  Diaconescu’s argument amounts to a derivation from AC4 (see above) of the assertion that every subset of a set is detachable, from which Excluded Middle readily follows. Here it is.