the carrier of (SubstLatt V,C) = SubstitutionSet V,C by Def4;
hence not SubstLatt V,C is empty ; :: thesis: verum