now :: thesis: for y being set st y in { y where y is Element of Y : [x,y] in E } holds
y in Y

let y be set ; :: thesis: ( y in { y where y is Element of Y : [x,y] in E } implies y in Y )
assume y in { y where y is Element of Y : [x,y] in E } ; :: thesis: y in Y
then ex y1 being Element of Y st
( y = y1 & [x,y1] in E ) ;
hence y in Y ; :: thesis: verum

end;

then { y where y is Element of Y : [x,y] in E } c= Y ;
hence { y where y is Element of Y : [x,y] in E } is Subset of Y ; :: thesis: verum