Assume all languages are over the alphabet \{0, 1\}.
coRe = \{L \in All : \bar L \in Re\}
\varepsilon, 0, 1, 00, 01, 10, 11, 000, 001, 010, \cdots
Each TM is represented by a finite string from \{0, 1\}^*. Since |\{0, 1\}^*| = \alef_0 then the set of TM is countable.
Let w_i be strings from \{0, 1\}^* in canonical order (input). Let \langle M_i \rangle be strings from \{0, 1\}^* in canonical order (codes of TM).
a_{ij} = \begin{cases} 1 & \text{if } w_i \in L(M_j) \\ 0 & \text{if } w_i \notin L(M_j) \\ \end{cases}
Then the diagonal language is L_d = \{w_i : a_{ij} = 0\} = \{w_i : w_i \notin L(M_i)\}
L_u = \{\langle M, w\rangle : w \in L(M)\}
L_e = \bar L_{ne}
L_r = \bar L_{nr}
One of the following conditions holds
A property of recursively enumerable languages is any set S \subseteq Re
Let S be a property of recursively enumerable languages, then L_s =\{\left\langle M \right\rangle : L(M) \in S\}
For any non-trivial property of recursively enumerable languages S. L_s \notin R.
Let S be a non-trivial property of recursively enumerable languages. There exists L \in S (since S is non-empty). Let M_L be a TM such that L(M_L) = L. Suppose L_S \in R then \bar L_S = L_{\bar S} \in R. We can assume that \emptyset \notin S without loss of generality (otherwise we consider \bar S). There exists a TM with stop property M_S such that L(M_S) = L_S. There exists an algorithm A that for a given input string \langle M, w \rangle constructs a code of a TM \langle M' \rangle such that
L(M') = \begin{cases} \emptyset & \text{if } w \notin L(M) \\ L & \text{if } w \in L(M) \\ \end{cases}
We can construct algorithm B such that L(B) = L_u.
\langle M, w \rangle \in L(B) \iff \langle M' \rangle \in L(M_S) \iff \langle M' \rangle \in L_S \iff L(M') \in S \iff L(M') = L \iff w \in L(M) \iff \langle M, w \rangle \in L_u