reconsider A = [#] T as a_union_of_components of T by Th20;
not A is empty ;
hence not for b₁ being a_union_of_components of T holds b₁ is empty ; :: thesis: verum