theorem Th24: :: DILWORTH:24

for R being transitive RelStr
for x being Element of R
for S being Subset of R st x is_minimal_in Lower S holds
x is_minimal_in [#] R