let A be Ordinal; :: thesis: A +^ 1 = succ A
thus A +^ 1 = succ (A +^ 0) by Lm1, Th28
.= succ A by Th27 ; :: thesis: verum