1 +^ 1 = succ (1 +^ {}) by Lm2, ORDINAL2:45
.= succ 1 by ORDINAL2:44
.= two ;
hence one + one = two by ARYTM_3:64; :: thesis: verum