let G be _Graph; :: thesis: for v being Vertex of G holds
( v .edgesIn() = (the_Target_of G) " {v} & v .edgesOut() = (the_Source_of G) " {v} )
let v be Vertex of G; :: thesis: ( v .edgesIn() = (the_Target_of G) " {v} & v .edgesOut() = (the_Source_of G) " {v} )

now :: thesis: for e being object holds
( ( e in v .edgesIn() implies e in (the_Target_of G) " {v} ) & ( e in (the_Target_of G) " {v} implies e in v .edgesIn() ) )

let e be object ; :: thesis: ( ( e in v .edgesIn() implies e in (the_Target_of G) " {v} ) & ( e in (the_Target_of G) " {v} implies e in v .edgesIn() ) )

hereby :: thesis: ( e in (the_Target_of G) " {v} implies e in v .edgesIn() )

assume e in v .edgesIn() ; :: thesis: e in (the_Target_of G) " {v}
then A1: ( e in the_Edges_of G & (the_Target_of G) . e = v ) by Lm7;
then A2: e in dom (the_Target_of G) by FUNCT_2:def 1;
(the_Target_of G) . e in {v} by A1, TARSKI:def 1;
hence e in (the_Target_of G) " {v} by A2, FUNCT_1:def 7; :: thesis: verum

end;

assume e in (the_Target_of G) " {v} ; :: thesis: e in v .edgesIn()
then A3: ( e in dom (the_Target_of G) & (the_Target_of G) . e in {v} ) by FUNCT_1:def 7;
then (the_Target_of G) . e = v by TARSKI:def 1;
hence e in v .edgesIn() by A3, Lm7; :: thesis: verum

end;

hence v .edgesIn() = (the_Target_of G) " {v} by TARSKI:2; :: thesis: v .edgesOut() = (the_Source_of G) " {v}

now :: thesis: for e being object holds
( ( e in v .edgesOut() implies e in (the_Source_of G) " {v} ) & ( e in (the_Source_of G) " {v} implies e in v .edgesOut() ) )

let e be object ; :: thesis: ( ( e in v .edgesOut() implies e in (the_Source_of G) " {v} ) & ( e in (the_Source_of G) " {v} implies e in v .edgesOut() ) )

hereby :: thesis: ( e in (the_Source_of G) " {v} implies e in v .edgesOut() )

assume e in v .edgesOut() ; :: thesis: e in (the_Source_of G) " {v}
then A4: ( e in the_Edges_of G & (the_Source_of G) . e = v ) by Lm8;
then A5: e in dom (the_Source_of G) by FUNCT_2:def 1;
(the_Source_of G) . e in {v} by A4, TARSKI:def 1;
hence e in (the_Source_of G) " {v} by A5, FUNCT_1:def 7; :: thesis: verum

end;

assume e in (the_Source_of G) " {v} ; :: thesis: e in v .edgesOut()
then A6: ( e in dom (the_Source_of G) & (the_Source_of G) . e in {v} ) by FUNCT_1:def 7;
then (the_Source_of G) . e = v by TARSKI:def 1;
hence e in v .edgesOut() by A6, Lm8; :: thesis: verum

end;

hence v .edgesOut() = (the_Source_of G) " {v} by TARSKI:2; :: thesis: verum