:: deftheorem defines loci_of ABCMIZ_1:def 22 :
for c being Element of Constructors holds loci_of c = (c `2) `1 ;