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 Th29;
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 Th26;
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 Th25;
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,XA8:
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, XBOOLE_0:def 8;
then
card (Edges_In v,X) < card (Edges_In v,the carrier' of G)
by CARD_2:67;
hence
Degree v <> Degree v,
X
by A4, A5, NAT_1:44, XREAL_1:10;
verum end; suppose A9:
v = the
Source of
G . e
;
Degree v <> Degree v,XA10:
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, XBOOLE_0:def 8;
then
card (Edges_Out v,X) < card (Edges_Out v,the carrier' of G)
by CARD_2:67;
hence
Degree v <> Degree v,
X
by A4, A6, NAT_1:44, XREAL_1:10;
verum end;