let a, b be Ordinal; :: thesis: a (+) (succ b) = succ (a (+) b)
thus a (+) (succ b) = a (+) (b (+) 1) by Th90
.= (a (+) b) (+) 1 by Th81
.= succ (a (+) b) by Th90 ; :: thesis: verum