let V, A be set ; :: thesis: for D being TypeSCNominativeData of V,A holds D in Union (FNDSC (V,A))
let D be TypeSCNominativeData of V,A; :: thesis: D in Union (FNDSC (V,A))
A1: ( D in A or D is NonatomicND of V,A ) by Def6;
A c= Union (FNDSC (V,A)) by Th11;
hence D in Union (FNDSC (V,A)) by A1, Th31; :: thesis: verum