not 3 is trivial by NAT_2:def 1;
hence not TriangularNumbers is empty ; :: thesis: verum