reconsider N = M as ManySortedSubset of M by PBOOLE:def 18;
reconsider N1 = N as OrderSortedSubset of M by Def1;
take N1 ; :: thesis: N1 is non-empty
thus N1 is non-empty ; :: thesis: verum