let G be _Graph; :: thesis: for v being Vertex of G
for e, w being object st v is isolated holds
not e Joins v,w,G
let v be Vertex of G; :: thesis: for e, w being object st v is isolated holds
not e Joins v,w,G
let e, w be object ; :: thesis: ( v is isolated implies not e Joins v,w,G )
assume v is isolated ; :: thesis: not e Joins v,w,G
then not e in v .edgesInOut() by GLIB_000:def 49;
hence not e Joins v,w,G by GLIB_000:62; :: thesis: verum