:: deftheorem defines Sierp36 NUMBER11:def 1 :
for n, s being Nat holds
( Sierp36 n,s iff ( Sum (digits (n,10)) = s & s divides n & ( for m being Nat st Sum (digits (m,10)) = s & s divides m holds
n <= m ) ) );