let a1, v, v1 be object ; :: thesis: for V, A being set st {v,v1} c= V & a1 in A holds

ND_ex_2 (v,v1,a1) is NonatomicND of V,A

let V, A be set ; :: thesis: ( {v,v1} c= V & a1 in A implies ND_ex_2 (v,v1,a1) is NonatomicND of V,A )

assume A1: ( {v,v1} c= V & a1 in A ) ; :: thesis: ND_ex_2 (v,v1,a1) is NonatomicND of V,A

take S = <*(NDSS (V,A)),(NDSS (V,(A \/ (NDSS (V,A)))))*>; :: according to NOMIN_1:def 5 :: thesis: ( S IsNDRankSeq V,A & ND_ex_2 (v,v1,a1) in Union S )

thus S IsNDRankSeq V,A by Th28; :: thesis: ND_ex_2 (v,v1,a1) in Union S

A2: Union S = (NDSS (V,A)) \/ (NDSS (V,(A \/ (NDSS (V,A))))) by FINSEQ_3:136;

ND_ex_2 (v,v1,a1) in NDSS (V,(A \/ (NDSS (V,A)))) by A1, Th48;

hence ND_ex_2 (v,v1,a1) in Union S by A2, XBOOLE_0:def 3; :: thesis: verum

ND_ex_2 (v,v1,a1) is NonatomicND of V,A

let V, A be set ; :: thesis: ( {v,v1} c= V & a1 in A implies ND_ex_2 (v,v1,a1) is NonatomicND of V,A )

assume A1: ( {v,v1} c= V & a1 in A ) ; :: thesis: ND_ex_2 (v,v1,a1) is NonatomicND of V,A

take S = <*(NDSS (V,A)),(NDSS (V,(A \/ (NDSS (V,A)))))*>; :: according to NOMIN_1:def 5 :: thesis: ( S IsNDRankSeq V,A & ND_ex_2 (v,v1,a1) in Union S )

thus S IsNDRankSeq V,A by Th28; :: thesis: ND_ex_2 (v,v1,a1) in Union S

A2: Union S = (NDSS (V,A)) \/ (NDSS (V,(A \/ (NDSS (V,A))))) by FINSEQ_3:136;

ND_ex_2 (v,v1,a1) in NDSS (V,(A \/ (NDSS (V,A)))) by A1, Th48;

hence ND_ex_2 (v,v1,a1) in Union S by A2, XBOOLE_0:def 3; :: thesis: verum