set d = Depth t;
t is (Depth t) + (0 * m) -termal by DefDepth2;
hence for b₁ being string of S st b₁ = t null m holds
b₁ is (Depth t) + m -termal ; :: thesis: verum