set X = Union (FNDSC (V,A));
take A \/ (Union (FNDSC (V,A))) ; :: thesis: for b₁ being set st ( b₁ in A or b₁ is NonatomicND of V,A ) holds
b₁ 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