theorem Th12: :: BAGORD_2:24

for R being non empty transitive asymmetric RelStr
for X being set st X is finite & ex x being Element of R st x in X holds
ex x being Element of R st x is_maximal_in X