the_sort_of A is Component of the Sorts of A by Def12;
hence not the_sort_of A is empty ; :: thesis: verum