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 non-empty )
thus ( C is Segre-like & C is trivial-yielding & C is non-empty ) ; :: thesis: verum