for x being set st x is Ordinal holds
succ x is Ordinal