let x be Element of X; :: thesis: x is DWalk of G
x in { W where W is DWalk of G : verum } ;
then ex y being DWalk of G st y = x ;
hence x is DWalk of G ; :: thesis: verum