let v be Vertex of KoenigsbergBridges; :: thesis: ( v = 3 implies Degree v = 3 )
assume v: v = 3 ; :: thesis: Degree v = 3
c1: Edges_In v = {30,60,70}

proof

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

proof

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

end;

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

proof

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

proof

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

end;

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in {} or a in Edges_Out v )
assume a in {} ; :: thesis: a in Edges_Out v
hence a in Edges_Out v ; :: thesis: verum

end;

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