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