theorem :: NOMIN_1:59
for a being object
for V, A being set
for f being b2 -valued FinSequence st len f > 0 holds
naming (V,A,f,a) is NonatomicND of V,A