let v be Vertex of KoenigsbergBridges; :: thesis: ( v = 0 implies Degree v = 3 )
assume v: v = 0 ; :: thesis: Degree v = 3

now :: thesis: for a being object holds not a in Edges_In v

let a be object ; :: thesis: not a in Edges_In v
reconsider s = a as set by TARSKI:1;
assume a in Edges_In v ; :: thesis: contradiction
then s: ( s in KEdges & KTarget . s = v ) by GRAPH_3:def 1;
dom KTarget = KEdges by FUNCT_2:def 1;
then s in dom KTarget by s;
then [s,v] in KTarget by s, FUNCT_1:1;
then ( [s,v] = [10,1] or [s,v] = [20,2] or [s,v] = [30,3] or [s,v] = [40,2] or [s,v] = [50,2] or [s,v] = [60,3] or [s,v] = [70,3] ) by ENUMSET1:def 5;
hence contradiction by v, XTUPLE_0:1; :: thesis: verum

end;

then c1: Edges_In v = {} by XBOOLE_0:def 1;
c2: Edges_Out v = {10,20,30}

proof

thus Edges_Out v c= {10,20,30} :: according to XBOOLE_0:def 10 :: thesis: {10,20,30} c= Edges_Out v

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in Edges_Out v or a in {10,20,30} )
reconsider s = a as set by TARSKI:1;
assume a in Edges_Out v ; :: thesis: a in {10,20,30}
then s: ( s in KEdges & KSource . s = v ) by GRAPH_3:def 2;
dom KSource = KEdges by FUNCT_2:def 1;
then s in dom KSource by s;
then [s,v] in KSource by s, FUNCT_1:1;
then ( [s,v] = [10,0] or [s,v] = [20,0] or [s,v] = [30,0] or [s,v] = [40,1] or [s,v] = [50,1] or [s,v] = [60,2] or [s,v] = [70,2] ) by ENUMSET1:def 5;
then ( s = 10 or s = 20 or s = 30 ) by v, XTUPLE_0:1;
hence a in {10,20,30} by ENUMSET1:def 1; :: thesis: verum

end;

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in {10,20,30} or a in Edges_Out v )
reconsider s = a as set by TARSKI:1;
assume a in {10,20,30} ; :: thesis: a in Edges_Out v
then a: ( a = 10 or a = 20 or a = 30 ) by ENUMSET1:def 1;
then s: s in KEdges by ENUMSET1:def 5;
[s,v] in KSource by v, a, ENUMSET1:def 5;
then KSource . s = v by FUNCT_1:1;
hence a in Edges_Out v by s, GRAPH_3:def 2; :: thesis: verum

end;

Degree (v, the carrier' of KoenigsbergBridges) = 0 + 3 by c1, c2, CARD_2:58;
hence Degree v = 3 by GRAPH_3:24; :: thesis: verum