let G be _trivial _Graph; :: thesis: ex v being Vertex of G st
( the_Vertices_of G = {v} & the_Source_of G = (the_Edges_of G) --> v & the_Target_of G = (the_Edges_of G) --> v )
consider v being Vertex of G such that
A1: the_Vertices_of G = {v} by GLIB_000:22;
take v ; :: thesis: ( the_Vertices_of G = {v} & the_Source_of G = (the_Edges_of G) --> v & the_Target_of G = (the_Edges_of G) --> v )
thus the_Vertices_of G = {v} by A1; :: thesis: ( the_Source_of G = (the_Edges_of G) --> v & the_Target_of G = (the_Edges_of G) --> v )
for e being object st e in dom (the_Source_of G) holds
(the_Source_of G) . e = v
proof
let e be object ; :: thesis: ( e in dom (the_Source_of G) implies (the_Source_of G) . e = v )
assume e in dom (the_Source_of G) ; :: thesis: (the_Source_of G) . e = v
then (the_Source_of G) . e in the_Vertices_of G by PARTFUN1:4;
hence (the_Source_of G) . e = v by A1, TARSKI:def 1; :: thesis: verum
end;
hence the_Source_of G = (dom (the_Source_of G)) --> v by FUNCOP_1:11
.= (the_Edges_of G) --> v by GLIB_000:4 ;
:: thesis: the_Target_of G = (the_Edges_of G) --> v
for e being object st e in dom (the_Target_of G) holds
(the_Target_of G) . e = v
proof
let e be object ; :: thesis: ( e in dom (the_Target_of G) implies (the_Target_of G) . e = v )
assume e in dom (the_Target_of G) ; :: thesis: (the_Target_of G) . e = v
then (the_Target_of G) . e in the_Vertices_of G by PARTFUN1:4;
hence (the_Target_of G) . e = v by A1, TARSKI:def 1; :: thesis: verum
end;
hence the_Target_of G = (dom (the_Target_of G)) --> v by FUNCOP_1:11
.= (the_Edges_of G) --> v by GLIB_000:4 ;
:: thesis: verum