theorem :: ORDINAL2:17

for A being Ordinal
for X being set st A in X holds
inf X in X