let v be Vertex of KoenigsbergBridges; :: thesis: ( v = 1 implies Degree v = 3 )
assume v: v = 1 ; :: thesis: Degree v = 3
c1: Edges_In v = {10}

proof

thus Edges_In v c= {10} :: according to XBOOLE_0:def 10 :: thesis: {10} c= Edges_In v

proof

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

end;

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

proof

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

proof

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

end;

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in {40,50} or a in Edges_Out v )
reconsider s = a as set by TARSKI:1;
assume a in {40,50} ; :: thesis: a in Edges_Out v
then a: ( a = 40 or a = 50 ) 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) = 1 & card (Edges_Out v) = 2 ) by c1, c2, CARD_1:30, CARD_2:57;
then Degree (v, the carrier' of KoenigsbergBridges) = 1 + 2 ;
hence Degree v = 3 by GRAPH_3:24; :: thesis: verum