:: deftheorem Def2 defines Domin_0 CATALAN2:def 2 :
for n, m being Nat
for b₃ being Subset of ({0,1} ^omega) holds
( b₃ = Domin_0 (n,m) iff for x being set holds
( x in b₃ iff ex p being XFinSequence of NAT st
( p = x & p is dominated_by_0 & dom p = n & Sum p = m ) ) );