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

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

end;

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