:: deftheorem defines IsNDRankSeq NOMIN_1:def 4 :
for V, A being set
for S being FinSequence holds
( S IsNDRankSeq V,A iff ( S . 1 = NDSS (V,A) & ( for n being Nat st n in dom S & n + 1 in dom S holds
S . (n + 1) = NDSS (V,(A \/ (S . n))) ) ) );