theorem Th25: :: DILWORTH:25

for R being transitive RelStr
for x being Element of R
for S being Subset of R st x is_maximal_in Upper S holds
x is_maximal_in [#] R