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

A1: now :: thesis: for e being object st e in { W where W is Trail of G : verum } holds
e in G .allWalks()

let e be object ; :: thesis: ( e in { W where W is Trail of G : verum } implies e in G .allWalks() )
assume e in { W where W is Trail of G : verum } ; :: thesis: e in G .allWalks()
then ex W being Trail of G st W = e ;
hence e in G .allWalks() ; :: thesis: verum

end;

G .walkOf the Element of the_Vertices_of G in { W where W is Trail of G : verum } ;
hence { W where W is Trail of G : verum } is non empty Subset of (G .allWalks()) by A1, TARSKI:def 3; :: thesis: verum