let V, A be set ; :: thesis: for D being NonatomicND of V,A holds D in Union (FNDSC (V,A))
let D be NonatomicND of V,A; :: thesis: D in Union (FNDSC (V,A))
ex S being FinSequence st
( S IsNDRankSeq V,A & D in Union S ) by Def5;
hence D in Union (FNDSC (V,A)) by Lm1; :: thesis: verum