Vamos supor $x \notin y$:

• $[\![ \check{x} \in \check{y} ]\!] = \sup_{t \in dom(\check{y})}\check{y}(t)[\![\check{x}=t]\!] = \sup_{t \in dom(\check{y})}\check{y}(t)[\![\check{x}\subseteq t]\!][\![t\subseteq \check{x}]\!]$
• Pela suposição $x \notin y$, assim para todo $a \in y$ temos que $a \not\subseteq x$ ou $x \not\subseteq a$, assim pela hipótese de indução temos :
  • $[\![\check{x}\subseteq \check{a}]\!]=0$ ou $[\![\check{a} \subseteq \check{x}]\!]=0$
  • Assim $[\![\check{x}\in \check{y}]\!]=0$ $\square$