A negation-free proof of Cantor's theorem (Q2565993)

The author gives a proof of Cantor's theorem according to which the power set \(P(X)\) of a set \(X\) exceeds the cardinality of \(X\). Assume that there is a bijective mapping \(M:X\to P(X)\). Then a sequence \(s_0,s_1, \dots\) is called a trace if \(s_0\in X\) is arbitrary, and if \(s_j\in M (s_{j-1})\) for \(j>0\). An element \(t\in X\) is said to be simple if all possible traces beginning with \(t\) terminate. Then it is shown that the set of simple elements cannot lie in the range of \(M\). So the proof constructs the leftover subset without explicitly invoking the negation operation.