hereby :: thesis: ( v .degree() = 0 implies v is isolated )
assume v is isolated ; :: thesis: v .degree() = 0
then A1: v .edgesInOut() = {} ;
then v .inDegree() = 0 by CARD_1:27, XBOOLE_1:15;
hence v .degree() = 0 by A1, CARD_1:27, XBOOLE_1:15; :: thesis: verum
end;
assume A2: v .degree() = 0 ; :: thesis: v is isolated
then v .edgesIn() = {} ;
hence v is isolated by A2; :: thesis: verum