let G1 be _finite _Graph; :: thesis: for e being set
for G2 being removeEdge of G1,e holds
( G1 .order() = G2 .order() & ( e in the_Edges_of G1 implies (G2 .size()) + 1 = G1 .size() ) )
let e be set ; :: thesis: for G2 being removeEdge of G1,e holds
( G1 .order() = G2 .order() & ( e in the_Edges_of G1 implies (G2 .size()) + 1 = G1 .size() ) )
let G2 be removeEdge of G1,e; :: thesis: ( G1 .order() = G2 .order() & ( e in the_Edges_of G1 implies (G2 .size()) + 1 = G1 .size() ) )
A1: the_Edges_of G2 = (the_Edges_of G1) \ {e} by Th51;
thus G1 .order() = G2 .order() by Th51; :: thesis: ( e in the_Edges_of G1 implies (G2 .size()) + 1 = G1 .size() )
assume e in the_Edges_of G1 ; :: thesis: (G2 .size()) + 1 = G1 .size()
then for x being object st x in {e} holds
x in the_Edges_of G1 by TARSKI:def 1;
then {e} c= the_Edges_of G1 ;
then A2: the_Edges_of G1 = (the_Edges_of G2) \/ {e} by A1, XBOOLE_1:45;
e in {e} by TARSKI:def 1;
then not e in the_Edges_of G2 by A1, XBOOLE_0:def 5;
hence (G2 .size()) + 1 = G1 .size() by A2, CARD_2:41; :: thesis: verum