for X, x being set holds
( x in FlatCoh X iff ( x = {} or ex y being set st
( x = {y} & y in X ) ) )