reconsider v = 0 as Vertex of KoenigsbergBridges by ENUMSET1:def 2;
Degree v = 3 by d0;
then not Degree v is even by POLYFORM:6;
hence for p being Path of KoenigsbergBridges holds
( not p is cyclic or not p is Eulerian ) by GRAPH_3:59; :: thesis: verum