let x be Element of X; :: thesis: x is DTrail of G

x in { W where W is DTrail of G : verum } ;

then ex y being DTrail of G st y = x ;

hence x is DTrail of G ; :: thesis: verum

x in { W where W is DTrail of G : verum } ;

then ex y being DTrail of G st y = x ;

hence x is DTrail of G ; :: thesis: verum