:: deftheorem defines tetrahedral NUMBER12:def 2 :
for n being Nat holds
( n is tetrahedral iff ex k being Nat st n = Tetrahedron k );