theorem :: ORDINAL2:22
for X, Y being set st X c= Y holds
sup X c= sup Y