:: deftheorem Def1 defines CastNat MODELC_2:def 1 :
for x being object holds
( ( x is Nat implies CastNat x = x ) & ( x is not Nat implies CastNat x = 0 ) );