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