reconsider N = the Sorts of U0 as MSSubset of U0 by PBOOLE:def 18;
the Sorts of U0 is OrderSortedSet of S by OSALG_1:17;
then reconsider M = N as OSSubset of U0 by Def2;
take M ; :: thesis: M is non-empty
thus M is non-empty ; :: thesis: verum