Suppose that `R[U]`, `F` is not in BCNF then exists `X->Y \in F^{+}` s.t. `X` is not a $superkey$ hence $F \nvDash$ `X->U` `=>` `\exists r` over `R[U]` s.t. $r \vDash F$ but $r \nvDash$ `X->U`, thence `\exists t_1, t_2 \in r : \pi_X(t_1) = \pi_X(t_2)` but `\pi_U(t_1)` $\neq$ `\pi_U(t_2)`.

Since `X->Y \in F^{+}` then $F \vDash$ `X->Y`, then `\pi_Y(t_1) = \pi_Y(t_2)` (because forall $s \vDash F$, $s \vDash$ `X->Y`, then in our particular `s = r` the claim holds).

Then: $\pi_X(t_1) = \pi_X(t_2)$ and $\pi_Y(t_1) = \pi_Y(t_2)$. Then: $\pi_{XY}(t_1) = \pi_{XY}(t_2)$.

We showed existence of `r` over `R[U]` s.t. `\exists t_1, t_2` s.t. `\pi_XY(t_1) = \pi_XY(t_2)`. Therefore `R[U], F` is `F^{+}` redundant.\[\begin{align} R(X) &\leftarrow S(X,Y),S(X,Z),\neg(Y=Z). && \text{UTF-8 is supported built-in} \\ R(X) &\leftarrow \neg R(X). && \text{עברית נתמכת באופן מובנה} \end{align}\]