:: deftheorem Def2 defines PeanoNat DTCONSTR:def 2 :
for b₁ being non empty strict DTConstrStr holds
( b₁ = PeanoNat iff ( the carrier of b₁ = {0,1} & ( for x being Symbol of b₁
for y being FinSequence of the carrier of b₁ holds
( x ==> y iff ( x = 1 & ( y = <*0*> or y = <*1*> ) ) ) ) ) );