let e, X be set ; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 A1:
( e in the carrier' of G & not e in X & ( v = the Target of G . e or v = the Source of G . e ) )
; :: thesis: Degree v <> Degree v,X
A2:
Degree v = Degree v,the carrier' of G
by Th29;
Edges_In v = Edges_In v,the carrier' of G
;
then A3:
Edges_In v,X c= Edges_In v,the carrier' of G
by Th25;
Edges_Out v = Edges_Out v,the carrier' of G
;
then A4:
Edges_Out v,X c= Edges_Out v,the carrier' of G
by Th26;
per cases
( v = the Target of G . e or v = the Source of G . e )
by A1;
suppose
v = the
Target of
G . e
;
:: thesis: Degree v <> Degree v,Xthen A5:
e in Edges_In v,the
carrier' of
G
by A1, Def1;
not
e in Edges_In v,
X
by A1, Def1;
then
Edges_In v,
X c< Edges_In v,the
carrier' of
G
by A3, A5, 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 A2, A4, NAT_1:44, XREAL_1:10;
:: thesis: verum end; suppose
v = the
Source of
G . e
;
:: thesis: Degree v <> Degree v,Xthen A6:
e in Edges_Out v,the
carrier' of
G
by A1, Def2;
not
e in Edges_Out v,
X
by A1, Def2;
then
Edges_Out v,
X c< Edges_Out v,the
carrier' of
G
by A4, A6, 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 A2, A3, NAT_1:44, XREAL_1:10;
:: thesis: verum end;