:: deftheorem defines succ ORDINAL1:def 1 :
for X being set holds succ X = X \/ {X};