let G be _Graph; :: thesis: for v1, e, v2 being object
for G1, G2 being addAdjVertex of G,v1,e,v2 holds G1 == G2
let v1, e, v2 be object ; :: thesis: for G1, G2 being addAdjVertex of G,v1,e,v2 holds G1 == G2
let G1, G2 be addAdjVertex of G,v1,e,v2; :: thesis: G1 == G2
per cases ( ( v1 in the_Vertices_of G & not v2 in the_Vertices_of G & not e in the_Edges_of G ) or ( not v1 in the_Vertices_of G & v2 in the_Vertices_of G & not e in the_Edges_of G ) or ( ( not v1 in the_Vertices_of G or v2 in the_Vertices_of G or e in the_Edges_of G ) & ( v1 in the_Vertices_of G or not v2 in the_Vertices_of G or e in the_Edges_of G ) ) ) ;
suppose ( v1 in the_Vertices_of G & not v2 in the_Vertices_of G & not e in the_Edges_of G ) ; :: thesis: G1 == G2
then ( the_Vertices_of G1 = (the_Vertices_of G) \/ {v2} & the_Edges_of G1 = (the_Edges_of G) \/ {e} & the_Source_of G1 = (the_Source_of G) +* (e .--> v1) & the_Target_of G1 = (the_Target_of G) +* (e .--> v2) & the_Vertices_of G2 = (the_Vertices_of G) \/ {v2} & the_Edges_of G2 = (the_Edges_of G) \/ {e} & the_Source_of G2 = (the_Source_of G) +* (e .--> v1) & the_Target_of G2 = (the_Target_of G) +* (e .--> v2) ) by Def12;
hence G1 == G2 by GLIB_000:def 34; :: thesis: verum
end;
suppose ( not v1 in the_Vertices_of G & v2 in the_Vertices_of G & not e in the_Edges_of G ) ; :: thesis: G1 == G2
then ( the_Vertices_of G1 = (the_Vertices_of G) \/ {v1} & the_Edges_of G1 = (the_Edges_of G) \/ {e} & the_Source_of G1 = (the_Source_of G) +* (e .--> v1) & the_Target_of G1 = (the_Target_of G) +* (e .--> v2) & the_Vertices_of G2 = (the_Vertices_of G) \/ {v1} & the_Edges_of G2 = (the_Edges_of G) \/ {e} & the_Source_of G2 = (the_Source_of G) +* (e .--> v1) & the_Target_of G2 = (the_Target_of G) +* (e .--> v2) ) by Def12;
hence G1 == G2 by GLIB_000:def 34; :: thesis: verum
end;
suppose ( ( not v1 in the_Vertices_of G or v2 in the_Vertices_of G or e in the_Edges_of G ) & ( v1 in the_Vertices_of G or not v2 in the_Vertices_of G or e in the_Edges_of G ) ) ; :: thesis: G1 == G2
then ( G == G1 & G == G2 ) by Def12;
hence G1 == G2 by GLIB_000:85; :: thesis: verum
end;
end;