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$ <wrap right>$\square$</wrap>