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