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

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