let V, A be set ; :: thesis: {} in NDSS (V,A)
{} is TypeSSNominativeData of V,A by RELSET_1:12;
hence {} in NDSS (V,A) ; :: thesis: verum