let v be Vertex of KoenigsbergBridges; ( v = 2 implies Degree v = 5 )
assume v:
v = 2
; Degree v = 5
c1:
Edges_In v = {20,40,50}
proof
thus
Edges_In v c= {20,40,50}
XBOOLE_0:def 10 {20,40,50} c= Edges_In vproof
let a be
object ;
TARSKI:def 3 ( 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
;
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;
verum
end;
let a be
object ;
TARSKI:def 3 ( 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}
;
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;
verum
end;
c2:
Edges_Out v = {60,70}
proof
thus
Edges_Out v c= {60,70}
XBOOLE_0:def 10 {60,70} c= Edges_Out vproof
let a be
object ;
TARSKI:def 3 ( 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
;
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;
verum
end;
let a be
object ;
TARSKI:def 3 ( not a in {60,70} or a in Edges_Out v )
reconsider s =
a as
set by TARSKI:1;
assume
a in {60,70}
;
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;
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; verum