let G be non edgeless _Graph; :: thesis: for e being Edge of G st not e in G .loops() holds
createGraph e in G .allForests()
let e be Edge of G; :: thesis: ( not e in G .loops() implies createGraph e in G .allForests() )
assume not e in G .loops() ; :: thesis: createGraph e in G .allForests()
then createGraph e is acyclic by Th18;
hence createGraph e in G .allForests() by Th78; :: thesis: verum