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