Depth ((l1,l2) -SymbolSubstIn phi) = Depth phi by Lm34;
hence for b₁ being set st b₁ = (Depth ((l1,l2) -SymbolSubstIn phi)) \+\ (Depth phi) holds
b₁ is empty ; :: thesis: verum