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