theorem :: ORDINAL3:2

for X, Y being set st succ X c= Y holds
X c= Y