:: deftheorem defines Y-section MEASUR11:def 5 :
for X, Y being set
for E being Subset of [:X,Y:]
for y being set holds Y-section (E,y) = { x where x is Element of X : [x,y] in E } ;