let G be _Graph; :: thesis: for v being Vertex of G holds
( v is isolated iff ( v .edgesIn() = {} & v .edgesOut() = {} ) )
let v be Vertex of G; :: thesis: ( v is isolated iff ( v .edgesIn() = {} & v .edgesOut() = {} ) )

hereby :: thesis: ( v .edgesIn() = {} & v .edgesOut() = {} implies v is isolated )

assume v is isolated ; :: thesis: ( v .edgesIn() = {} & v .edgesOut() = {} )
then v .edgesInOut() = {} by GLIB_000:def 49;
hence ( v .edgesIn() = {} & v .edgesOut() = {} ) ; :: thesis: verum

end;

assume ( v .edgesIn() = {} & v .edgesOut() = {} ) ; :: thesis: v is isolated
then v .edgesInOut() = {} ;
hence v is isolated by GLIB_000:def 49; :: thesis: verum