let G be _Graph; :: thesis: for e being set
for v1, v2 being Vertex of G st e Joins v1,v2,G holds
( v1 .adj e = v2 & v2 .adj e = v1 )
let e be set ; :: thesis: for v1, v2 being Vertex of G st e Joins v1,v2,G holds
( v1 .adj e = v2 & v2 .adj e = v1 )
let v1, v2 be Vertex of G; :: thesis: ( e Joins v1,v2,G implies ( v1 .adj e = v2 & v2 .adj e = v1 ) )
assume A1: e Joins v1,v2,G ; :: thesis: ( v1 .adj e = v2 & v2 .adj e = v1 )
then A2: e in v1 .edgesInOut() by Th65;
now
per cases ( ( (the_Source_of G) . e = v2 & (the_Target_of G) . e = v1 ) or ( (the_Source_of G) . e = v1 & (the_Target_of G) . e = v2 ) ) by A1, Def15;
suppose A3: ( (the_Source_of G) . e = v2 & (the_Target_of G) . e = v1 ) ; :: thesis: ( v1 .adj e = v2 & v2 .adj e = v1 )
hence v1 .adj e = v2 by A2, Def43; :: thesis: v2 .adj e = v1
now
per cases ( v1 = v2 or v1 <> v2 ) ;
suppose v1 = v2 ; :: thesis: v2 .adj e = v1
hence v2 .adj e = v1 by A2, A3, Def43; :: thesis: verum
end;
suppose v1 <> v2 ; :: thesis: v2 .adj e = v1
hence v2 .adj e = v1 by A2, A3, Def43; :: thesis: verum
end;
end;
end;
hence v2 .adj e = v1 ; :: thesis: verum
end;
suppose A4: ( (the_Source_of G) . e = v1 & (the_Target_of G) . e = v2 ) ; :: thesis: ( v1 .adj e = v2 & v2 .adj e = v1 )
now
per cases ( v1 = v2 or v1 <> v2 ) ;
suppose v1 = v2 ; :: thesis: v1 .adj e = v2
hence v1 .adj e = v2 by A2, A4, Def43; :: thesis: verum
end;
suppose v1 <> v2 ; :: thesis: v1 .adj e = v2
hence v1 .adj e = v2 by A2, A4, Def43; :: thesis: verum
end;
end;
end;
hence v1 .adj e = v2 ; :: thesis: v2 .adj e = v1
thus v2 .adj e = v1 by A2, A4, Def43; :: thesis: verum
end;
end;
end;
hence ( v1 .adj e = v2 & v2 .adj e = v1 ) ; :: thesis: verum