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