theorem :: ORDINAL3:72

for X being set holds sup X c= succ (union (On X))