for n being Element of NAT holds VERUM <> prop n