let G1, G2 be _Graph; :: thesis: for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 & G1 == G2 holds
( ( v1 is isolated implies v2 is isolated ) & ( v1 is endvertex implies v2 is endvertex ) )
let v1 be Vertex of G1; :: thesis: for v2 being Vertex of G2 st v1 = v2 & G1 == G2 holds
( ( v1 is isolated implies v2 is isolated ) & ( v1 is endvertex implies v2 is endvertex ) )
let v2 be Vertex of G2; :: thesis: ( v1 = v2 & G1 == G2 implies ( ( v1 is isolated implies v2 is isolated ) & ( v1 is endvertex implies v2 is endvertex ) ) )
assume A1: ( v1 = v2 & G1 == G2 ) ; :: thesis: ( ( v1 is isolated implies v2 is isolated ) & ( v1 is endvertex implies v2 is endvertex ) )

hereby :: thesis: ( v1 is endvertex implies v2 is endvertex )

assume v1 is isolated ; :: thesis: v2 is isolated
then v1 .edgesInOut() = {} by Def51;
then v2 .edgesInOut() = {} by A1, Th99;
hence v2 is isolated by Def51; :: thesis: verum

end;

assume v1 is endvertex ; :: thesis: v2 is endvertex
then consider e being set such that
A2: ( v1 .edgesInOut() = {e} & not e Joins v1,v1,G1 ) by Def53;
( v2 .edgesInOut() = {e} & not e Joins v2,v2,G2 ) by A1, A2, Th91, Th99;
hence v2 is endvertex by Def53; :: thesis: verum