let V, A be set ; <*(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; verum