theorem Th25: :: DICKSON:26

for R being non empty RelStr
for N being non empty Subset of R
for B being set st B is_Dickson-basis_of N,R holds
not B is empty