let V, A be set ; :: thesis: {} is NonatomicND of V,A
take S = <*(NDSS (V,A))*>; :: according to NOMIN_1:def 5 :: thesis: ( S IsNDRankSeq V,A & {} in Union S )
Union S = NDSS (V,A) by FINSEQ_3:135;
then the PartFunc of V,A | {} in Union S ;
hence ( S IsNDRankSeq V,A & {} in Union S ) by Th27; :: thesis: verum