let a, a1, v, v1, v2 be object ; for V, A being set st {v,v1,v2} c= V & {a,a1} c= A holds
ND_ex_4 (v,v1,v2,a,a1) is NonatomicND of V,A
let V, A be set ; ( {v,v1,v2} c= V & {a,a1} c= A implies ND_ex_4 (v,v1,v2,a,a1) is NonatomicND of V,A )
assume A1:
( {v,v1,v2} c= V & {a,a1} c= A )
; ND_ex_4 (v,v1,v2,a,a1) is NonatomicND of V,A
set R = ND_ex_4 (v,v1,v2,a,a1);
set S1 = NDSS (V,A);
set S2 = NDSS (V,(A \/ (NDSS (V,A))));
ND_ex_4 (v,v1,v2,a,a1) in NDSS (V,(A \/ (NDSS (V,A))))
by A1, Th54;
then A2:
ND_ex_4 (v,v1,v2,a,a1) in (NDSS (V,A)) \/ (NDSS (V,(A \/ (NDSS (V,A)))))
by XBOOLE_0:def 3;
Union <*(NDSS (V,A)),(NDSS (V,(A \/ (NDSS (V,A)))))*> = (NDSS (V,A)) \/ (NDSS (V,(A \/ (NDSS (V,A)))))
by FINSEQ_3:136;
hence
ND_ex_4 (v,v1,v2,a,a1) is NonatomicND of V,A
by A2, Def5, Th28; verum