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