reconsider N = M as ManySortedSubset of M by Def18;
take N ; :: thesis: N is non-empty
thus N is non-empty ; :: thesis: verum