:: deftheorem defines @ TRIANG_1:def 4 :
for n being Nat
for f being Element of Funcs ((Seg n),(Seg (n + 1))) holds @ f = f;