let G be _Graph; :: thesis: for v being Vertex of G holds
( v is isolated iff v .degree() = 0 )
let v be Vertex of G; :: thesis: ( v is isolated iff v .degree() = 0 )
hereby :: thesis: ( v .degree() = 0 implies v is isolated )
assume v is isolated ; :: thesis: v .degree() = 0
then ( v .inDegree() = 0 & v .outDegree() = 0 ) by Th38;
hence v .degree() = 0 +` 0
.= 0 ;
:: thesis: verum
end;
assume A1: v .degree() = 0 ; :: thesis: v is isolated
( v .inDegree() c= v .degree() & v .outDegree() c= v .degree() ) by CARD_2:94;
then ( v .inDegree() = 0 & v .outDegree() = 0 ) by A1;
hence v is isolated by Th38; :: thesis: verum