let G be _Graph; :: thesis: for e being set
for v being Vertex of G holds
( e in v .edgesInOut() iff e Joins v,v .adj e,G )
let e be set ; :: thesis: for v being Vertex of G holds
( e in v .edgesInOut() iff e Joins v,v .adj e,G )
let v be Vertex of G; :: thesis: ( e in v .edgesInOut() iff e Joins v,v .adj e,G )
hereby :: thesis: ( e Joins v,v .adj e,G implies e in v .edgesInOut() )
assume A1: e in v .edgesInOut() ; :: thesis: e Joins v,v .adj e,G
then A2: ( (the_Source_of G) . e = v or (the_Target_of G) . e = v ) by Th61;
now :: thesis: e Joins v,v .adj e,G
per cases ( (the_Target_of G) . e = v or (the_Target_of G) . e <> v ) ;
suppose A3: (the_Target_of G) . e = v ; :: thesis: e Joins v,v .adj e,G
then v .adj e = (the_Source_of G) . e by A1, Def41;
hence e Joins v,v .adj e,G by A1, A3; :: thesis: verum
end;
suppose A4: (the_Target_of G) . e <> v ; :: thesis: e Joins v,v .adj e,G
then v .adj e = (the_Target_of G) . e by A1, A2, Def41;
hence e Joins v,v .adj e,G by A1, A2, A4; :: thesis: verum
end;
end;
end;
hence e Joins v,v .adj e,G ; :: thesis: verum
end;
assume e Joins v,v .adj e,G ; :: thesis: e in v .edgesInOut()
hence e in v .edgesInOut() by Th62; :: thesis: verum