let G be loopless trivial _Graph; :: thesis: the_Edges_of G = {}
consider v being Vertex of G such that
A1: the_Vertices_of G = {v} by Th25;

now

assume the_Edges_of G <> {} ; :: thesis: contradiction
then consider e being set such that
A2: e in the_Edges_of G by XBOOLE_0:def 1;
(the_Target_of G) . e in {v} by A1, A2, FUNCT_2:5;
then A3: (the_Target_of G) . e = v by TARSKI:def 1;
(the_Source_of G) . e in {v} by A1, A2, FUNCT_2:5;
then (the_Source_of G) . e = v by TARSKI:def 1;
hence contradiction by A2, A3, Def20; :: thesis: verum

end;

hence the_Edges_of G = {} ; :: thesis: verum