let G be _trivial _Graph; for v being Vertex of G holds
( v .edgesIn() = the_Edges_of G & v .edgesOut() = the_Edges_of G & v .edgesInOut() = the_Edges_of G )
let v be Vertex of G; ( v .edgesIn() = the_Edges_of G & v .edgesOut() = the_Edges_of G & v .edgesInOut() = the_Edges_of G )
consider v0 being Vertex of G such that
A1:
the_Vertices_of G = {v0}
by GLIB_000:22;
A2:
v = v0
by A1, TARSKI:def 1;
A3:
now for e being object st e in the_Edges_of G holds
e DJoins v,v,Glet e be
object ;
( e in the_Edges_of G implies e DJoins v,v,G )assume A4:
e in the_Edges_of G
;
e DJoins v,v,Gthen
e Joins (the_Source_of G) . e,
(the_Target_of G) . e,
G
by GLIB_000:def 13;
then
(
(the_Source_of G) . e in the_Vertices_of G &
(the_Target_of G) . e in the_Vertices_of G )
by GLIB_000:13;
then
(
(the_Source_of G) . e = v0 &
(the_Target_of G) . e = v0 )
by A1, TARSKI:def 1;
hence
e DJoins v,
v,
G
by A2, A4, GLIB_000:def 14;
verum end;
for e being object st e in the_Edges_of G holds
e in v .edgesIn()
by A3, GLIB_000:57;
then
the_Edges_of G c= v .edgesIn()
by TARSKI:def 3;
hence A5:
v .edgesIn() = the_Edges_of G
by XBOOLE_0:def 10; ( v .edgesOut() = the_Edges_of G & v .edgesInOut() = the_Edges_of G )
for e being object st e in the_Edges_of G holds
e in v .edgesOut()
by A3, GLIB_000:59;
then
the_Edges_of G c= v .edgesOut()
by TARSKI:def 3;
hence
v .edgesOut() = the_Edges_of G
by XBOOLE_0:def 10; v .edgesInOut() = the_Edges_of G
hence
v .edgesInOut() = the_Edges_of G
by A5; verum