:: deftheorem defines `11 MCART_1:def 14 :
for x being object holds x `11 = (x `1) `1 ;