set IT = { W where W is DPath of G : verum } ;
A1: G .walkOf (choose (the_Vertices_of G)) in { W where W is DPath of G : verum } ;

now

let e be set ; :: 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 consider W being DPath of G such that
A2: e = W ;
thus e in G .allDTrails() by A2; :: thesis: verum

end;

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