:: deftheorem Def1 defines CHK SIN_COS:def 1 :
for m, k being natural Number holds
( ( m <= k implies CHK (m,k) = 1 ) & ( not m <= k implies CHK (m,k) = 0 ) );