theorem Th30: :: DICKSON:31

for R being non empty RelStr st R is quasi_ordered & ( for f being sequence of R ex i, j being Nat st
( i < j & f . i <= f . j ) ) holds
for N being non empty Subset of R holds
( min-classes N is finite & not min-classes N is empty )