:: deftheorem Def1 defines min* NAT_1:def 1 :
for A being set
for b₂ being Element of NAT holds
( ( A is non empty Subset of NAT implies ( b₂ = min* A iff ( b₂ in A & ( for k being Nat st k in A holds
b₂ <= k ) ) ) ) & ( A is not non empty Subset of NAT implies ( b₂ = min* A iff b₂ = 0 ) ) );