is mentioned by

Thm* eq:{T=}, L,M:T List. L(eq)M (x:{x:T| x(eq) L }. x(eq) M)

[is_intersection_implies_exists_element]