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