let V, A be set ; :: thesis: <*(NDSS (V,A)),(NDSS (V,(A \/ (NDSS (V,A))))),(NDSS (V,(A \/ (NDSS (V,(A \/ (NDSS (V,A))))))))*> IsNDRankSeq V,A
set S = <*(NDSS (V,A)),(NDSS (V,(A \/ (NDSS (V,A)))))*>;
( len <*(NDSS (V,A)),(NDSS (V,(A \/ (NDSS (V,A)))))*> = 2 & <*(NDSS (V,A)),(NDSS (V,(A \/ (NDSS (V,A)))))*> . 2 = NDSS (V,(A \/ (NDSS (V,A)))) ) by FINSEQ_1:44;
hence <*(NDSS (V,A)),(NDSS (V,(A \/ (NDSS (V,A))))),(NDSS (V,(A \/ (NDSS (V,(A \/ (NDSS (V,A))))))))*> IsNDRankSeq V,A by Th17, Th28; :: thesis: verum