$[\![ \forall y \in \dot{x} \varphi(y) ]\!]$

$\displaystyle =\inf_{t}[\![ t \in \dot{x} \Longrightarrow \varphi(t) ]\!]$

$\displaystyle =\inf_{t}(-[\![ t \in \dot{x} ]\!]+[\![ \varphi(t) ]\!])$

$\displaystyle =\inf_{t}([\![ \varphi(t) ]\!]+-\sup_{y \in \text{dom}(\dot{x})}[\![ t=y ]\!] \dot{x}(y))$

$\displaystyle =\inf_{t}([\![ \varphi(t)]\!]+\inf_{y \in \text{dom}(\dot{x})}(-[\![t=y]\!]+-\dot{x}(y)))$

$\displaystyle =\inf_{t}\inf_{y \in \text{dom}(\dot{x})}([\![\varphi(t)]\!]+-[\![t=y]\!]+-\dot{x}(y))$

$\displaystyle =\inf_{y \in \text{dom}(\dot{x})}\inf_{t}(-\dot{x}(y)+-[\![t=y]\!]+[\![\varphi(t)]\!])$

$\displaystyle =\inf_{y \in \text{dom}(\dot{x})}(-\dot{x}(y)+\inf_{t}(-[\![t=y]\!]+-[\![¬\varphi(t)]\!]))$

$\displaystyle =\inf_{y \in \text{dom}(\dot{x})}(-\dot{x}(y)+-\sup_{t}[\![t=y]\!][\![¬\varphi(t)]\!])$

$\displaystyle =\inf_{y \in \text{dom}(\dot{x})}(-\dot{x}(y)+-[\![¬\varphi(y)]\!])$

$\displaystyle =\inf_{y \in \text{dom}(\dot{x})}(-\dot{x}(y)+[\![\varphi(y)]\!])$

$\displaystyle =\inf_{y \in \text{dom}(\dot{x})}(\dot{x}(y)\Longrightarrow[\![\varphi(y)]\!])$