[{} ,0 ] in { [{} ,i] where i is Element of NAT : verum } ;
hence not Vars is empty by Th16; :: thesis: verum