let G1 be _Graph; :: thesis: for G2 being Subgraph of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 & v1 is endvertex & not v2 is endvertex holds
v2 is isolated
let G2 be Subgraph of G1; :: thesis: for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 & v1 is endvertex & not v2 is endvertex holds
v2 is isolated
let v1 be Vertex of G1; :: thesis: for v2 being Vertex of G2 st v1 = v2 & v1 is endvertex & not v2 is endvertex holds
v2 is isolated
let v2 be Vertex of G2; :: thesis: ( v1 = v2 & v1 is endvertex & not v2 is endvertex implies v2 is isolated )
assume that
A1: v1 = v2 and
A2: v1 is endvertex ; :: thesis: ( v2 is endvertex or v2 is isolated )
consider e being object such that
A3: v1 .edgesInOut() = {e} and
A4: not e Joins v1,v1,G1 by A2;
v2 .edgesInOut() c= v1 .edgesInOut() by A1, Th78;
then A5: ( v2 .edgesInOut() = {} or v2 .edgesInOut() = {e} ) by A3, ZFMISC_1:33;
( not v2 is isolated implies v2 is endvertex ) by A5, A1, A4, Lm4;
hence ( v2 is endvertex or v2 is isolated ) ; :: thesis: verum