hereby :: thesis: ( v .degree() = 0 implies v is isolated )

assume v is isolated ; :: thesis: v .degree() = 0
then v .edgesInOut() = {} by Def51;
then ( v .inDegree() = 0 & v .outDegree() = 0 ) by CARD_1:47, XBOOLE_1:15;
hence v .degree() = 0 ; :: thesis: verum

end;

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