set IT = { W where W is DPath of G : verum } ;

hence { W where W is directed Path of G : verum } is non empty Subset of (G .allDTrails()) by A1, TARSKI:def 3; :: thesis: verum

A1: now :: thesis: for e being object st e in { W where W is DPath of G : verum } holds

e in G .allDTrails()

G .walkOf the Element of the_Vertices_of G in { W where W is DPath of G : verum }
;e in G .allDTrails()

let e be object ; :: thesis: ( e in { W where W is DPath of G : verum } implies e in G .allDTrails() )

assume e in { W where W is DPath of G : verum } ; :: thesis: e in G .allDTrails()

then ex W being DPath of G st e = W ;

hence e in G .allDTrails() ; :: thesis: verum

end;assume e in { W where W is DPath of G : verum } ; :: thesis: e in G .allDTrails()

then ex W being DPath of G st e = W ;

hence e in G .allDTrails() ; :: thesis: verum

hence { W where W is directed Path of G : verum } is non empty Subset of (G .allDTrails()) by A1, TARSKI:def 3; :: thesis: verum