:: deftheorem defines Tetrahedron NUMBER12:def 1 :
for n being Nat holds Tetrahedron n = ((n * (n + 1)) * (n + 2)) / 6;