{} in t by TREES_1:22;
hence ex b₁ being Element of t st b₁ is empty ; :: thesis: verum