{{}} in SubstitutionSet (V,C) by Th2;
hence not for b₁ being Element of SubstitutionSet (V,C) holds b₁ is empty ; :: thesis: verum