:: deftheorem defines `12 MCART_1:def 15 :
for x being object holds x `12 = (x `1) `2 ;