reconsider B = the Sorts of U0 as MSSubset of U0 by PBOOLE:def 18;
take B ; :: thesis: B is OrderSortedSet of S
thus B is OrderSortedSet of S by OSALG_1:17; :: thesis: verum