let G be _Graph; :: thesis: for v being Vertex of G holds
( v is isolated iff ( v .inDegree() = 0 & v .outDegree() = 0 ) )
let v be Vertex of G; :: thesis: ( v is isolated iff ( v .inDegree() = 0 & v .outDegree() = 0 ) )

hereby :: thesis: ( v .inDegree() = 0 & v .outDegree() = 0 implies v is isolated )

assume v is isolated ; :: thesis: ( v .inDegree() = 0 & v .outDegree() = 0 )
then ( v .edgesIn() = {} & v .edgesOut() = {} ) ;
hence ( v .inDegree() = 0 & v .outDegree() = 0 ) ; :: thesis: verum

end;

assume ( v .inDegree() = 0 & v .outDegree() = 0 ) ; :: thesis: v is isolated
then ( v .edgesIn() = {} & v .edgesOut() = {} ) ;
hence v is isolated ; :: thesis: verum