budu dokazovat dve implikace:

→

dle schematu specifikace (za A_x[t] vezmu A_x[x]):

(∀x)(∀y)A -> (∀y)A
(∀y)A -> A

tedy (slozeni implikaci):

(∀x)(∀y)A -> A

pravidlo generalizace:

(∀x)[(∀x)(∀y)A -> A]

v (∀x)(∀y)A urcite neni x volne, tedy muzu pouzit schema preskoku:

(∀x)(∀y)A -> (∀x)A

pravidlo generalizace:

(∀y)[(∀x)(∀y)A -> (∀x)A]

schema preskoku:

(∀x)(∀y)A -> (∀y)(∀x)A

←

analogicky... :)

(pozn.: je to psane jen tak narychlo, kdyztak to nekdo vylepsete... :) )