let D be NonatomicND of V,A; :: thesis: D is finite
ex n being Nat st D is TypeSSNominativeData of V,(A \/ ((FNDSC (V,A)) . n)) by Th33;
hence D is finite ; :: thesis: verum