:: deftheorem defines `22 MCART_1:def 17 :
for x being object holds x `22 = (x `2) `2 ;