theorem :: ORDINAL6:3

for X being ordinal-membered set holds X c= sup X by ORDINAL2:19;