let G be _Graph; :: thesis: for e, x, y being set st e Joins x,y,G holds
( x in the_Vertices_of G & y in the_Vertices_of G )
let e, x, y be set ; :: thesis: ( e Joins x,y,G implies ( x in the_Vertices_of G & y in the_Vertices_of G ) )
assume A1: e Joins x,y,G ; :: thesis: ( x in the_Vertices_of G & y in the_Vertices_of G )
then A2: ( ( (the_Source_of G) . e = x & (the_Target_of G) . e = y ) or ( (the_Source_of G) . e = y & (the_Target_of G) . e = x ) ) by Def15;
e in the_Edges_of G by A1, Def15;
hence ( x in the_Vertices_of G & y in the_Vertices_of G ) by A2, FUNCT_2:5; :: thesis: verum