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 Th22;
now :: thesis: not the_Edges_of G <> {}
assume the_Edges_of G <> {} ; :: thesis: contradiction
then consider e being object 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, Def18; :: thesis: verum
end;
hence the_Edges_of G = {} ; :: thesis: verum