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