theorem Th33: :: DILWORTH:33

for R being RelStr
for S being Subset of R
for B being Subset of (subrelstr S)
for x being Element of (subrelstr S)
for y being Element of R st x = y & x is_minimal_in B holds
y is_minimal_in B