theorem :: ORDINAL2:24

for X being set holds inf X c= sup X