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