let a, v be object ; :: thesis: for V, A being set st v in V & a in A holds

ND_ex_1 (v,a) is NonatomicND of V,A

let V, A be set ; :: thesis: ( v in V & a in A implies ND_ex_1 (v,a) is NonatomicND of V,A )

assume A1: ( v in V & a in A ) ; :: thesis: ND_ex_1 (v,a) is NonatomicND of V,A

take S = <*(NDSS (V,A))*>; :: according to NOMIN_1:def 5 :: thesis: ( S IsNDRankSeq V,A & ND_ex_1 (v,a) in Union S )

thus S IsNDRankSeq V,A by Th27; :: thesis: ND_ex_1 (v,a) in Union S

ND_ex_1 (v,a) in NDSS (V,A) by A1, Th45;

hence ND_ex_1 (v,a) in Union S by FINSEQ_3:135; :: thesis: verum

ND_ex_1 (v,a) is NonatomicND of V,A

let V, A be set ; :: thesis: ( v in V & a in A implies ND_ex_1 (v,a) is NonatomicND of V,A )

assume A1: ( v in V & a in A ) ; :: thesis: ND_ex_1 (v,a) is NonatomicND of V,A

take S = <*(NDSS (V,A))*>; :: according to NOMIN_1:def 5 :: thesis: ( S IsNDRankSeq V,A & ND_ex_1 (v,a) in Union S )

thus S IsNDRankSeq V,A by Th27; :: thesis: ND_ex_1 (v,a) in Union S

ND_ex_1 (v,a) in NDSS (V,A) by A1, Th45;

hence ND_ex_1 (v,a) in Union S by FINSEQ_3:135; :: thesis: verum