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 V8()
thus M is V8() ; :: thesis: verum