theorem Th70: :: NUMPOLY1:70

for x being number holds
( x in TriangularNumbers iff x is triangular )