let a, a1, v, v1 be object ; :: thesis: for V, A being set st {v,v1} c= V & {a,a1} c= A holds
ND_ex_3 (v,v1,a,a1) is NonatomicND of V,A
let V, A be set ; :: thesis: ( {v,v1} c= V & {a,a1} c= A implies ND_ex_3 (v,v1,a,a1) is NonatomicND of V,A )
assume A1: ( {v,v1} c= V & {a,a1} c= A ) ; :: thesis: ND_ex_3 (v,v1,a,a1) is NonatomicND of V,A
take <*(NDSS (V,A))*> ; :: according to NOMIN_1:def 5 :: thesis: ( <*(NDSS (V,A))*> IsNDRankSeq V,A & ND_ex_3 (v,v1,a,a1) in Union <*(NDSS (V,A))*> )
thus <*(NDSS (V,A))*> IsNDRankSeq V,A by Th27; :: thesis: ND_ex_3 (v,v1,a,a1) in Union <*(NDSS (V,A))*>
ND_ex_3 (v,v1,a,a1) in NDSS (V,A) by A1, Th51;
hence ND_ex_3 (v,v1,a,a1) in Union <*(NDSS (V,A))*> by FINSEQ_3:135; :: thesis: verum