given p being Path of KoenigsbergBridges such that p: ( not p is cyclic & p is Eulerian ) ; :: thesis: contradiction
consider v1, v2 being Vertex of KoenigsbergBridges such that
v: ( v1 <> v2 & ( for v being Vertex of KoenigsbergBridges holds
( Degree v is even iff ( v <> v1 & v <> v2 ) ) ) ) by p, GRAPH_3:60;
( ( v1 = 0 or v1 = 1 or v1 = 2 or v1 = 3 ) & ( v2 = 0 or v2 = 1 or v2 = 2 or v2 = 3 ) & v1 <> v2 ) by v, ENUMSET1:def 2;

per cases then ( ( v1 = 0 & v2 = 1 ) or ( v1 = 0 & v2 = 2 ) or ( v1 = 1 & v2 = 0 ) or ( v1 = 1 & v2 = 2 ) or ( v1 = 2 & v2 = 0 ) or ( v1 = 2 & v2 = 1 ) or ( v1 = 1 & v2 = 3 ) or ( v1 = 2 & v2 = 3 ) or ( v1 = 3 & v2 = 1 ) or ( v1 = 3 & v2 = 2 ) or ( v1 = 0 & v2 = 3 ) or ( v1 = 3 & v2 = 0 ) ) ;

suppose s: ( ( v1 = 0 & v2 = 1 ) or ( v1 = 0 & v2 = 2 ) or ( v1 = 1 & v2 = 0 ) or ( v1 = 1 & v2 = 2 ) or ( v1 = 2 & v2 = 0 ) or ( v1 = 2 & v2 = 1 ) ) ; :: thesis: contradiction

reconsider v = 3 as Vertex of KoenigsbergBridges by ENUMSET1:def 2;
Degree v = 3 by d3;
then not Degree v is even by POLYFORM:6;
hence contradiction by s, v; :: thesis: verum

end;

suppose s: ( ( v1 = 1 & v2 = 3 ) or ( v1 = 2 & v2 = 3 ) or ( v1 = 3 & v2 = 1 ) or ( v1 = 3 & v2 = 2 ) ) ; :: thesis: contradiction

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 contradiction by s, v; :: thesis: verum

end;

suppose s: ( ( v1 = 0 & v2 = 3 ) or ( v1 = 3 & v2 = 0 ) ) ; :: thesis: contradiction

reconsider v = 1 as Vertex of KoenigsbergBridges by ENUMSET1:def 2;
Degree v = 3 by d1;
then not Degree v is even by POLYFORM:6;
hence contradiction by s, v; :: thesis: verum

end;

end;