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 Th156;
hence v .degree() = card (0 + 0) by CARD_2:38
.= 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, XBOOLE_1:3;
hence v is isolated by Th156; :: thesis: verum