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