theorem Th20: :: DICKSON:21

for R being non empty RelStr
for N being Subset of R
for y being Element of (R \~) st y is_minimal_wrt N, the InternalRel of (R \~) holds
not min-classes N is empty