reconsider N = M as ManySortedSubset of M by Def18;
take N ; :: thesis: N is V8()
thus N is V8() ; :: thesis: verum