:: deftheorem Def1 defines k_id MODELC_1:def 1 :
for x being object
for S being set
for a being Element of S holds
( ( x in S implies k_id (x,S,a) = x ) & ( not x in S implies k_id (x,S,a) = a ) );