:: deftheorem defines index_of ABCMIZ_1:def 23 :
for c being Element of Constructors holds index_of c = (c `2) `2 ;