let G be _Graph; :: thesis: for X being set
for v being Vertex of G st v is isolated holds
G .edgesBetween (X \ {v}) = G .edgesBetween X
let X be set ; :: thesis: for v being Vertex of G st v is isolated holds
G .edgesBetween (X \ {v}) = G .edgesBetween X
let v be Vertex of G; :: thesis: ( v is isolated implies G .edgesBetween (X \ {v}) = G .edgesBetween X )
assume A1: v is isolated ; :: thesis: G .edgesBetween (X \ {v}) = G .edgesBetween X
thus G .edgesBetween (X \ {v}) = (G .edgesBetween X) \ (v .edgesInOut()) by Th107
.= G .edgesBetween X by A1 ; :: thesis: verum