reconsider X = M as ManySortedSubset of M by PBOOLE:def 23;
take X ; :: thesis: X is OrderSortedSet of
thus X is OrderSortedSet of ; :: thesis: verum