let a be Ordinal; :: thesis: a (+) 1 = succ a
thus a (+) 1 = a +^ 1 by Th88
.= succ a by ORDINAL2:31 ; :: thesis: verum