theorem :: ZF_REFLE:18

for X being set holds sup X c= succ (union (On X)) by ORDINAL3:72;