is mentioned by

Thm* f:(TProp), c:Collection(T), x:T. x < i c | f(i) > x c & f(x)

[member_col_filter]

Try larger context: GenAutomata