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