:: deftheorem Def2 defines k_nat MODELC_1:def 2 :
for x being object holds
( ( x in NAT implies k_nat x = x ) & ( not x in NAT implies k_nat x = 0 ) );