1 +^ 1 = succ (1 +^ {}) by Lm2, ORDINAL2:28
.= succ 1 by ORDINAL2:27
.= two ;
hence one + one = two by ARYTM_3:58; :: thesis: verum