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

hence { W where W is Walk of G : verum } is non empty Subset of (((the_Vertices_of G) \/ (the_Edges_of G)) *) by A1, TARSKI:def 3; :: thesis: verum

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

x in ((the_Vertices_of G) \/ (the_Edges_of G)) *

G .walkOf the Element of the_Vertices_of G in { W where W is Walk of G : verum }
;x in ((the_Vertices_of G) \/ (the_Edges_of G)) *

let x be object ; :: thesis: ( x in { W where W is Walk of G : verum } implies x in ((the_Vertices_of G) \/ (the_Edges_of G)) * )

assume x in { W where W is Walk of G : verum } ; :: thesis: x in ((the_Vertices_of G) \/ (the_Edges_of G)) *

then ex W being Walk of G st x = W ;

hence x in ((the_Vertices_of G) \/ (the_Edges_of G)) * by FINSEQ_1:def 11; :: thesis: verum

end;assume x in { W where W is Walk of G : verum } ; :: thesis: x in ((the_Vertices_of G) \/ (the_Edges_of G)) *

then ex W being Walk of G st x = W ;

hence x in ((the_Vertices_of G) \/ (the_Edges_of G)) * by FINSEQ_1:def 11; :: thesis: verum

hence { W where W is Walk of G : verum } is non empty Subset of (((the_Vertices_of G) \/ (the_Edges_of G)) *) by A1, TARSKI:def 3; :: thesis: verum