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 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 ) ; :: thesis: 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 ; :: thesis: 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; :: thesis: verum

end;

suppose A9: v = the Source of G . e ; :: thesis: 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; :: thesis: verum

end;

end;