let i be Nat; :: thesis: [{},i] in Vars
i in NAT by ORDINAL1:def 12;
then [{},i] in { [{},j] where j is Element of NAT : verum } ;
hence [{},i] in Vars by Th16; :: thesis: verum