set B = the Element of Carrier A;
reconsider C = { the Element of Carrier A} as ManySortedSubset of Carrier A by Th11;
take C ; :: thesis: ( C is Segre-like & C is trivial-yielding & C is V2() )
thus ( C is Segre-like & C is trivial-yielding & C is V2() ) ; :: thesis: verum