:: deftheorem Def3 defines len ALGSEQ_1:def 3 :
for R being non empty ZeroStr
for p being AlgSequence of R
for b₃ being Element of NAT holds
( b₃ = len p iff ( b₃ is_at_least_length_of p & ( for m being Nat st m is_at_least_length_of p holds
b₃ <= m ) ) );