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

ex n being Nat st D is TypeSSNominativeData of V,(A \/ ((FNDSC (V,A)) . n)) by Th33;

hence D is finite ; :: thesis: verum