set Y = the V2() ManySortedSubset of T;
take the V2() ManySortedSubset of T ; :: thesis: the V2() ManySortedSubset of T is V2()
thus the V2() ManySortedSubset of T is V2() ; :: thesis: verum