:: deftheorem Def5 defines NonatomicND NOMIN_1:def 5 :
for V, A being set
for b₃ being Function holds
( b₃ is NonatomicND of V,A iff ex S being FinSequence st
( S IsNDRankSeq V,A & b₃ in Union S ) );