2 |^|^ 3 = 2 |^ (2 |^ 2) by Th3;
hence 13 = (2 |^|^ (0 + 3)) - 3 by Lm1, Lm3
.= H₁(4, 0 ) by Th12 ;
:: thesis: verum