Coim (E,y) = E " {y} ;
hence Y-section (E,y) is Subset of X ; :: thesis: verum