let G1 be _Graph; :: thesis: for G3 being SimpleGraph of G1 ex G2 being removeParallelEdges of G1 st G3 is removeLoops of G2
let G3 be SimpleGraph of G1; :: thesis: ex G2 being removeParallelEdges of G1 st G3 is removeLoops of G2
consider E being RepEdgeSelection of G1 such that
A1: G3 is inducedSubgraph of G1, the_Vertices_of G1,E \ (G1 .loops()) by Def9;
set G2 = the inducedSubgraph of G1, the_Vertices_of G1,E;
reconsider G2 = the inducedSubgraph of G1, the_Vertices_of G1,E as removeParallelEdges of G1 by Def7;
take G2 ; :: thesis: G3 is removeLoops of G2
A2: ( the_Vertices_of G1 c= the_Vertices_of G1 & the_Edges_of G1 = G1 .edgesBetween () ) by GLIB_000:34;
then A3: ( the_Vertices_of G3 = the_Vertices_of G1 & the_Edges_of G3 = E \ (G1 .loops()) ) by ;
A4: ( the_Vertices_of G2 = the_Vertices_of G1 & the_Edges_of G2 = E ) by ;
A5: the_Vertices_of G3 = the_Vertices_of G2 by A3, A4;
for e being object holds
( e in the_Edges_of G3 iff e in () \ (G2 .loops()) )
proof
let e be object ; :: thesis: ( e in the_Edges_of G3 iff e in () \ (G2 .loops()) )
hereby :: thesis: ( e in () \ (G2 .loops()) implies e in the_Edges_of G3 )
assume e in the_Edges_of G3 ; :: thesis: e in () \ (G2 .loops())
then A6: ( e in the_Edges_of G2 & not e in G1 .loops() ) by ;
not e in G2 .loops()
proof
assume e in G2 .loops() ; :: thesis: contradiction
then consider v being object such that
A7: e Joins v,v,G2 by Def2;
( e is set & v is set ) by TARSKI:1;
then e Joins v,v,G1 by ;
hence contradiction by A6, Def2; :: thesis: verum
end;
hence e in () \ (G2 .loops()) by ; :: thesis: verum
end;
assume e in () \ (G2 .loops()) ; :: thesis:
then A8: ( e in the_Edges_of G2 & not e in G2 .loops() ) by XBOOLE_0:def 5;
not e in G1 .loops()
proof
assume e in G1 .loops() ; :: thesis: contradiction
then consider v being object such that
A9: e Joins v,v,G1 by Def2;
( e is set & v is set ) by TARSKI:1;
then e Joins v,v,G2 by ;
hence contradiction by A8, Def2; :: thesis: verum
end;
hence e in the_Edges_of G3 by ; :: thesis: verum
end;
then A10: the_Edges_of G3 = () \ (G2 .loops()) by TARSKI:2;
E \ (G1 .loops()) c= E by XBOOLE_1:36;
then A11: G3 is Subgraph of G2 by ;
( the_Vertices_of G2 c= the_Vertices_of G2 & the_Edges_of G2 = G2 .edgesBetween () ) by GLIB_000:34;
hence G3 is removeLoops of G2 by ; :: thesis: verum