let v be Vertex of KoenigsbergBridges; :: thesis: ( v = 2 implies Degree v = 5 )
assume v: v = 2 ; :: thesis: Degree v = 5
c1: Edges_In v = {20,40,50}

proof

thus Edges_In v c= {20,40,50} :: according to XBOOLE_0:def 10 :: thesis: {20,40,50} c= Edges_In v

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in Edges_In v or a in {20,40,50} )
reconsider s = a as set by TARSKI:1;
assume a in Edges_In v ; :: thesis: a in {20,40,50}
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;
then ( s = 20 or s = 40 or s = 50 ) by v, XTUPLE_0:1;
hence a in {20,40,50} by ENUMSET1:def 1; :: thesis: verum

end;

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

end;

c2: Edges_Out v = {60,70}

proof

thus Edges_Out v c= {60,70} :: according to XBOOLE_0:def 10 :: thesis: {60,70} c= Edges_Out v

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in Edges_Out v or a in {60,70} )
reconsider s = a as set by TARSKI:1;
assume a in Edges_Out v ; :: thesis: a in {60,70}
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 = 60 or s = 70 ) by v, XTUPLE_0:1;
hence a in {60,70} by TARSKI:def 2; :: thesis: verum

end;

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in {60,70} or a in Edges_Out v )
reconsider s = a as set by TARSKI:1;
assume a in {60,70} ; :: thesis: a in Edges_Out v
then a: ( a = 60 or a = 70 ) by TARSKI:def 2;
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;

( card (Edges_In v) = 3 & card (Edges_Out v) = 2 ) by c1, c2, CARD_2:57, CARD_2:58;
then Degree (v, the carrier' of KoenigsbergBridges) = 3 + 2 ;
hence Degree v = 5 by GRAPH_3:24; :: thesis: verum