let G be _trivial _Graph; :: thesis: 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; :: thesis: ( 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 Th22;
A2: v = v0 by A1, TARSKI:def 1;

A3: now :: thesis: for e being object st e in the_Edges_of G holds
e DJoins v,v,G

let e be object ; :: thesis: ( e in the_Edges_of G implies e DJoins v,v,G )
assume A4: e in the_Edges_of G ; :: thesis: e DJoins v,v,G
then e Joins (the_Source_of G) . e,(the_Target_of G) . e,G ;
then ( (the_Source_of G) . e in the_Vertices_of G & (the_Target_of G) . e in the_Vertices_of G ) by FUNCT_2:5;
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; :: thesis: verum

end;

for e being object st e in the_Edges_of G holds
e in v .edgesIn() by A3, Th57;
then the_Edges_of G c= v .edgesIn() ;
hence A5: v .edgesIn() = the_Edges_of G by XBOOLE_0:def 10; :: thesis: ( 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, Th59;
then the_Edges_of G c= v .edgesOut() ;
hence v .edgesOut() = the_Edges_of G by XBOOLE_0:def 10; :: thesis: v .edgesInOut() = the_Edges_of G
hence v .edgesInOut() = the_Edges_of G by A5; :: thesis: verum