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() = {} by GLIB_000:def 49;
then (v .edgesIn()) \/ (v .edgesOut()) = {} by GLIB_000:60;
then ( v .edgesIn() = {} & v .edgesOut() = {} ) ;
then ( (the_Source_of G) .: (v .edgesIn()) = {} & (the_Target_of G) .: (v .edgesOut()) = {} ) ;
then ( v .inNeighbors() = {} & v .outNeighbors() = {} ) by GLIB_000:def 46, GLIB_000:def 47;
then (v .inNeighbors()) \/ (v .outNeighbors()) = {} \/ {} ;
hence v .allNeighbors() = {} by GLIB_000:def 48; :: thesis: verum
end;
assume A1: v .allNeighbors() = {} ; :: thesis: v is isolated
assume not v is isolated ; :: thesis: contradiction
then A2: v .edgesInOut() <> {} by GLIB_000:def 49;
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, GLIB_000:64;
thus contradiction by A1, A3, GLIB_000:71; :: thesis: verum