theorem :: ORDINAL2:14

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