is mentioned by

Thm* s:(A+B) List, x:A. (x mapoutl(s)) (y:A+B. (y s) & isl(y) & x = outl(y))	[member_mapoutl]
Def mapoutl(s) == mapfilter(x.outl(x);x.isl(x);s)	[mapoutl]

In prior sections: union

Try larger context: Graphs