let V be non empty set ; :: thesis: for E being Relation of V holds createGraph (V,(E \ (id V))) is removeLoops of (createGraph (V,E))
let E be Relation of V; :: thesis: createGraph (V,(E \ (id V))) is removeLoops of (createGraph (V,E))
set G = createGraph (V,E);
set H = createGraph (V,(E \ (id V)));
V c= V ;
then A1: createGraph (V,(E \ (id V))) is inducedSubgraph of createGraph (V,E),V,E \ (id V) by XBOOLE_1:36, GLUNIR00:85;
(the_Edges_of (createGraph (V,E))) \ ((createGraph (V,E)) .loops()) = E \ ((createGraph (V,E)) .loops())
.= E \ (E /\ (id V)) by Th130
.= E \ (id V) by XBOOLE_1:47 ;
hence createGraph (V,(E \ (id V))) is removeLoops of (createGraph (V,E)) by A1; :: thesis: verum