set X = Union (FNDSC (V,A));

take A \/ (Union (FNDSC (V,A))) ; :: thesis: for b_{1} being set st ( b_{1} in A or b_{1} is NonatomicND of V,A ) holds

b_{1} in A \/ (Union (FNDSC (V,A)))

let x be set ; :: thesis: ( ( x in A or x is NonatomicND of V,A ) implies x in A \/ (Union (FNDSC (V,A))) )

assume ( x in A or x is NonatomicND of V,A ) ; :: thesis: x in A \/ (Union (FNDSC (V,A)))

then ( x in A or ( x is Function & ex S being FinSequence st

( S IsNDRankSeq V,A & x in Union S ) ) ) by Def5;

then ( x in A or x in Union (FNDSC (V,A)) ) by Lm1;

hence x in A \/ (Union (FNDSC (V,A))) by XBOOLE_0:def 3; :: thesis: verum

take A \/ (Union (FNDSC (V,A))) ; :: thesis: for b

b

let x be set ; :: thesis: ( ( x in A or x is NonatomicND of V,A ) implies x in A \/ (Union (FNDSC (V,A))) )

assume ( x in A or x is NonatomicND of V,A ) ; :: thesis: x in A \/ (Union (FNDSC (V,A)))

then ( x in A or ( x is Function & ex S being FinSequence st

( S IsNDRankSeq V,A & x in Union S ) ) ) by Def5;

then ( x in A or x in Union (FNDSC (V,A)) ) by Lm1;

hence x in A \/ (Union (FNDSC (V,A))) by XBOOLE_0:def 3; :: thesis: verum