let G be non edgeless _Graph; :: thesis: for E being set
for e being Edge of G
for H being removeEdges of G,E st not e in E holds
createGraph e is Subgraph of H
let E be set ; :: thesis: for e being Edge of G
for H being removeEdges of G,E st not e in E holds
createGraph e is Subgraph of H
let e be Edge of G; :: thesis: for H being removeEdges of G,E st not e in E holds
createGraph e is Subgraph of H
let H be removeEdges of G,E; :: thesis: ( not e in E implies createGraph e is Subgraph of H )
assume A1: not e in E ; :: thesis: createGraph e is Subgraph of H
the_Vertices_of G = the_Vertices_of H by GLIB_000:def 33;
then A2: the_Vertices_of (createGraph e) c= the_Vertices_of H ;
the_Edges_of H = (the_Edges_of G) \ E by GLIB_000:53;
then e in the_Edges_of H by A1, XBOOLE_0:def 5;
then {e} c= the_Edges_of H by ZFMISC_1:31;
then the_Edges_of (createGraph e) c= the_Edges_of H by Th13;
hence createGraph e is Subgraph of H by A2, GLIB_000:44; :: thesis: verum