2 |^|^ 4 = 2 |^ (2 |^ (2 |^ 2)) by Th4;
hence 65533 = (2 |^|^ (1 + 3)) - 3 by Lm1, Lm3, Lm4
.= H₁(4,1) by Th12 ;
:: thesis: verum