for I being non empty set
for A being PLS-yielding ManySortedSet of I st ( for i being Element of I holds A . i is strongly_connected ) holds
for B being set holds
( B is Segre-Coset of A iff ex W being Subset of (Segre_Product A) st
( not W is trivial & W is strong & W is closed_under_lines & B = union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & W,Y are_joinable ) } ) )