Durch Existenzeinführung im Sukzedenz haben wir
und
und daraus
Dabei ist y {\displaystyle {}y} hinten gebunden und somit kann man mit der Existenzeinführung im Antezedens auf
schließen. Da auch x {\displaystyle {}x} hinten gebunden ist, ergibt sich