set Y = the non-empty ManySortedSubset of T;
take the non-empty ManySortedSubset of T ; :: thesis: the non-empty ManySortedSubset of T is non-empty
thus the non-empty ManySortedSubset of T is non-empty ; :: thesis: verum