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