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