|.(ar t0).| = 0 ;
hence for b₁ being Element of (AllTermsOf S) * st b₁ = SubTerms t0 holds
b₁ is empty ; :: thesis: verum