reconsider N = M as ManySortedSubset of M by PBOOLE:def 18;
reconsider N1 = N as OrderSortedSubset of M by Def1;
take N1 ; :: thesis: N1 is V8()
thus N1 is V8() ; :: thesis: verum