:: deftheorem Def4 defines dseq IRRAT_1:def 4 :
for b₁ being Real_Sequence holds
( b₁ = dseq iff for n being Nat holds b₁ . n = (1 + (1 / n)) ^ n );