let e, X be set ; for G being finite Graph
for v being Vertex of G st e in the carrier' of G & not e in X & ( v = the Target of G . e or v = the Source of G . e ) holds
Degree v <> Degree (v,X)
let G be finite Graph; for v being Vertex of G st e in the carrier' of G & not e in X & ( v = the Target of G . e or v = the Source of G . e ) holds
Degree v <> Degree (v,X)
let v be Vertex of G; ( e in the carrier' of G & not e in X & ( v = the Target of G . e or v = the Source of G . e ) implies Degree v <> Degree (v,X) )
set T = the Target of G;
set S = the Source of G;
set E = the carrier' of G;
assume that
A1:
e in the carrier' of G
and
A2:
not e in X
and
A3:
( v = the Target of G . e or v = the Source of G . e )
; Degree v <> Degree (v,X)
A4:
Degree v = Degree (v, the carrier' of G)
by Th24;
Edges_Out v = Edges_Out (v, the carrier' of G)
;
then A5:
Edges_Out (v,X) c= Edges_Out (v, the carrier' of G)
by Th21;
Edges_In v = Edges_In (v, the carrier' of G)
;
then A6:
Edges_In (v,X) c= Edges_In (v, the carrier' of G)
by Th20;
per cases
( v = the Target of G . e or v = the Source of G . e )
by A3;
suppose A7:
v = the
Target of
G . e
;
Degree v <> Degree (v,X)A8:
not
e in Edges_In (
v,
X)
by A2, Def1;
e in Edges_In (
v, the
carrier' of
G)
by A1, A7, Def1;
then
Edges_In (
v,
X)
c< Edges_In (
v, the
carrier' of
G)
by A6, A8;
then
card (Edges_In (v,X)) < card (Edges_In (v, the carrier' of G))
by CARD_2:48;
hence
Degree v <> Degree (
v,
X)
by A4, A5, NAT_1:43, XREAL_1:8;
verum end; suppose A9:
v = the
Source of
G . e
;
Degree v <> Degree (v,X)A10:
not
e in Edges_Out (
v,
X)
by A2, Def2;
e in Edges_Out (
v, the
carrier' of
G)
by A1, A9, Def2;
then
Edges_Out (
v,
X)
c< Edges_Out (
v, the
carrier' of
G)
by A5, A10;
then
card (Edges_Out (v,X)) < card (Edges_Out (v, the carrier' of G))
by CARD_2:48;
hence
Degree v <> Degree (
v,
X)
by A4, A6, NAT_1:43, XREAL_1:8;
verum end;