theorem :: ORDINAL3:1

for X being set holds X c= succ X by XBOOLE_1:7;