theorem :: ABCMIZ_1:28

for i being Nat
for x being variable holds [((vars x) \/ {x}),i] in Vars