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