:: deftheorem Def6 defines Step1 ASYMPT_1:def 7 :
for x being Nat
for b₂ being Element of NAT holds
( ( x <> 0 implies ( b₂ = Step1 x iff ex n being Element of NAT st
( n ! <= x & x < (n + 1) ! & b₂ = n ! ) ) ) & ( not x <> 0 implies ( b₂ = Step1 x iff b₂ = 0 ) ) );