let V, A be set ; :: thesis: <*(NDSS (V,A)),(NDSS (V,(A \/ (NDSS (V,A)))))*> IsNDRankSeq V,A
A1: <*(NDSS (V,A))*> IsNDRankSeq V,A by Th27;
len <*(NDSS (V,A))*> = 1 by FINSEQ_1:40;
hence <*(NDSS (V,A)),(NDSS (V,(A \/ (NDSS (V,A)))))*> IsNDRankSeq V,A by A1, Th17; :: thesis: verum