theorem :: ABCMIZ_1:25

for i being Nat holds [{},i] in Vars