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