let G be _Graph; :: thesis: for e, x1, y1, x2, y2 being set st e Joins x1,y1,G & e Joins x2,y2,G & not ( x1 = x2 & y1 = y2 ) holds
( x1 = y2 & y1 = x2 )
let e, x1, y1, x2, y2 be set ; :: thesis: ( e Joins x1,y1,G & e Joins x2,y2,G & not ( x1 = x2 & y1 = y2 ) implies ( x1 = y2 & y1 = x2 ) )
assume that
A1: e Joins x1,y1,G and
A2: e Joins x2,y2,G ; :: thesis: ( ( x1 = x2 & y1 = y2 ) or ( x1 = y2 & y1 = x2 ) )
set S = (the_Source_of G) . e;
set T = (the_Target_of G) . e;

now

per cases ( ( (the_Source_of G) . e = x1 & (the_Target_of G) . e = y1 ) or ( (the_Source_of G) . e = y1 & (the_Target_of G) . e = x1 ) ) by A1, Def15;

suppose A3: ( (the_Source_of G) . e = x1 & (the_Target_of G) . e = y1 ) ; :: thesis: ( ( x1 = x2 & y1 = y2 ) or ( x1 = y2 & y1 = x2 ) )

now

per cases ( ( (the_Source_of G) . e = x2 & (the_Target_of G) . e = y2 ) or ( (the_Source_of G) . e = y2 & (the_Target_of G) . e = x2 ) ) by A2, Def15;

suppose ( (the_Source_of G) . e = x2 & (the_Target_of G) . e = y2 ) ; :: thesis: ( ( x1 = x2 & y1 = y2 ) or ( x1 = y2 & y1 = x2 ) )

hence ( ( x1 = x2 & y1 = y2 ) or ( x1 = y2 & y1 = x2 ) ) by A3; :: thesis: verum

end;

suppose ( (the_Source_of G) . e = y2 & (the_Target_of G) . e = x2 ) ; :: thesis: ( ( x1 = x2 & y1 = y2 ) or ( x1 = y2 & y1 = x2 ) )

hence ( ( x1 = x2 & y1 = y2 ) or ( x1 = y2 & y1 = x2 ) ) by A3; :: thesis: verum

end;

end;

end;

hence ( ( x1 = x2 & y1 = y2 ) or ( x1 = y2 & y1 = x2 ) ) ; :: thesis: verum

end;

suppose A4: ( (the_Source_of G) . e = y1 & (the_Target_of G) . e = x1 ) ; :: thesis: ( ( x1 = x2 & y1 = y2 ) or ( x1 = y2 & y1 = x2 ) )

now

per cases ( ( (the_Source_of G) . e = x2 & (the_Target_of G) . e = y2 ) or ( (the_Source_of G) . e = y2 & (the_Target_of G) . e = x2 ) ) by A2, Def15;

suppose ( (the_Source_of G) . e = x2 & (the_Target_of G) . e = y2 ) ; :: thesis: ( ( x1 = x2 & y1 = y2 ) or ( x1 = y2 & y1 = x2 ) )

hence ( ( x1 = x2 & y1 = y2 ) or ( x1 = y2 & y1 = x2 ) ) by A4; :: thesis: verum

end;

suppose ( (the_Source_of G) . e = y2 & (the_Target_of G) . e = x2 ) ; :: thesis: ( ( x1 = x2 & y1 = y2 ) or ( x1 = y2 & y1 = x2 ) )

hence ( ( x1 = x2 & y1 = y2 ) or ( x1 = y2 & y1 = x2 ) ) by A4; :: thesis: verum

end;

end;

end;

hence ( ( x1 = x2 & y1 = y2 ) or ( x1 = y2 & y1 = x2 ) ) ; :: thesis: verum

end;

end;

end;

hence ( ( x1 = x2 & y1 = y2 ) or ( x1 = y2 & y1 = x2 ) ) ; :: thesis: verum