:: deftheorem Def2 defines Nat MIDSP_3:def 2 :
for n, b₂ being Nat holds
( b₂ is Nat of n iff ( 1 <= b₂ & b₂ <= n + 1 ) );