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 isolated 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 isolated holds
v2 is isolated
let v1 be Vertex of G1; :: thesis: for v2 being Vertex of G2 st v1 = v2 & v1 is isolated holds
v2 is isolated
let v2 be Vertex of G2; :: thesis: ( v1 = v2 & v1 is isolated implies v2 is isolated )
assume ( v1 = v2 & v1 is isolated ) ; :: thesis: v2 is isolated
then ( v1 .edgesInOut() = {} & v2 .edgesInOut() c= v1 .edgesInOut() ) by Th78;
hence v2 is isolated ; :: thesis: verum