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 ) )
hence ( v1 is isolated implies v2 is isolated ) by Th96; :: thesis: ( v1 is endvertex implies v2 is endvertex )
assume v1 is endvertex ; :: thesis: v2 is endvertex
then consider e being object such that
A2: ( v1 .edgesInOut() = {e} & not e Joins v1,v1,G1 ) ;
( v2 .edgesInOut() = {e} & not e Joins v2,v2,G2 ) by A1, A2, Th96;
hence v2 is endvertex ; :: thesis: verum