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

hereby :: thesis: ( v .allNeighbors() = {} implies v is isolated )

assume v is isolated ; :: thesis: v .allNeighbors() = {}
then v .edgesInOut() = {} ;
then (v .edgesIn()) \/ (v .edgesOut()) = {} ;
then ( v .edgesIn() = {} & v .edgesOut() = {} ) ;
then ( (the_Source_of G) .: (v .edgesIn()) = {} & (the_Target_of G) .: (v .edgesOut()) = {} ) ;
then ( v .inNeighbors() = {} & v .outNeighbors() = {} ) ;
then (v .inNeighbors()) \/ (v .outNeighbors()) = {} \/ {} ;
hence v .allNeighbors() = {} ; :: thesis: verum

end;

assume A1: v .allNeighbors() = {} ; :: thesis: v is isolated
assume not v is isolated ; :: thesis: contradiction
then A2: v .edgesInOut() <> {} ;
set e = the Element of v .edgesInOut() ;
consider v0 being Vertex of G such that
A3: the Element of v .edgesInOut() Joins v,v0,G by A2, Th64;
thus contradiction by A1, A3, Th71; :: thesis: verum